TRS: {c() -> f(), f() -> g()} RPO Product: Quasi-Precedence: c > f empty Qed TRS: {c() -> f(), f() -> g()} Cdiprover: Interpretation class: quasisimplemixed Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING g = + 0 c = + 2 f = + 2 Qed