YES TRS: { f(x, x) -> a(), f(g(x), y) -> f(x, y)} RUF: Strict: {f(x, x) -> a()} Weak: {} RUF: Strict: {} Weak: {} Qed