YES TRS: {f(0(), 1(), x) -> f(x, x, x)} DP: Strict: {f#(0(), 1(), x) -> f#(x, x, x)} Weak: {f(0(), 1(), x) -> f(x, x, x)} EDG: {} SCCS: Qed