3.13/1.75 YES 3.13/1.75 3.13/1.75 Proof: 3.13/1.75 This system is confluent. 3.13/1.75 Inlined conditions in System R. 3.13/1.75 By \cite{ALS94}, Theorem 4.1. 3.13/1.75 This system is of type 3 or smaller. 3.13/1.75 This system is strongly deterministic. 3.13/1.75 This system is quasi-decreasing. 3.13/1.75 By \cite{A14}, Theorem 11.5.9. 3.13/1.75 This system is of type 3 or smaller. 3.13/1.75 This system is deterministic. 3.13/1.75 System R transformed to V(R) + Emb. 3.13/1.75 This system is terminating. 3.13/1.75 Call external tool: 3.13/1.75 ./ttt2.sh 3.13/1.75 Input: 3.13/1.75 (VAR x) 3.13/1.75 (RULES 3.13/1.75 f(x) -> g(x) 3.13/1.75 g(x) -> x 3.13/1.75 f(x) -> x 3.13/1.75 ) 3.13/1.75 3.13/1.75 KBO Processor: 3.13/1.75 weight function: 3.13/1.75 w0 = 1 3.13/1.75 w(g) = w(f) = 1 3.13/1.75 precedence: 3.13/1.75 f > g 3.13/1.75 problem: 3.13/1.75 3.13/1.75 Qed 3.13/1.75 All 0 critical pairs are joinable. 3.13/1.75 3.61/1.79 EOF