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