YES Proof: This system is quasi-decreasing. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: a -> c g(a) -> h(b) h(b) -> g(c) f(x) -> g(x) h(x) -> x g(x) -> x f(x) -> x LPO Processor: precedence: f > a > b > h ~ g ~ c problem: Qed