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