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