YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: pin(a) -> pout(b) pin(b) -> pout(c) tc(x) -> x ?2(y, x) -> y ?1(pout(z), x) -> ?2(tc(z), x) tc(x) -> ?1(pin(x), x) LPO Processor: precedence: a > b > pout > tc > ?1 > z ~ ?2 ~ c ~ pin problem: Qed