⁶All we say here applies also to rewrite theories with an additional freezing function ϕ specifying which arguments of each function symbol are frozen.