3.01/1.65 YES 3.01/1.65 3.01/1.65 Proof: 3.01/1.65 This system is confluent. 3.01/1.65 Removed infeasible rules from system R. 3.01/1.65 By \cite{ALS94}, Theorem 4.1. 3.01/1.65 This system is of type 3 or smaller. 3.01/1.65 This system is strongly deterministic. 3.01/1.65 This system is quasi-decreasing. 3.01/1.65 By \cite{O02}, p. 214, Proposition 7.2.50. 3.01/1.65 This system is of type 3 or smaller. 3.01/1.65 This system is deterministic. 3.01/1.65 System R transformed to U(R). 3.01/1.65 This system is terminating. 3.01/1.65 Call external tool: 3.01/1.65 ./ttt2.sh 3.01/1.65 Input: 3.01/1.65 (VAR ) 3.01/1.65 (RULES 3.01/1.65 3.01/1.65 ) 3.01/1.65 3.01/1.66 Bounds Processor: 3.01/1.66 bound: 0 3.01/1.66 enrichment: match 3.01/1.66 automaton: 3.01/1.66 final states: {2} 3.01/1.66 transitions: 3.01/1.66 f20() -> 2* 3.01/1.66 problem: 3.01/1.66 3.01/1.66 Qed 3.01/1.66 All 0 critical pairs are joinable. 3.01/1.66 3.37/1.72 EOF