1.99/1.64 YES 1.99/1.64 1.99/1.64 Proof: 1.99/1.64 This system is confluent. 1.99/1.64 By \cite{ALS94}, Theorem 4.1. 1.99/1.64 This system is of type 3 or smaller. 1.99/1.64 This system is strongly deterministic. 1.99/1.64 This system is quasi-decreasing. 1.99/1.64 By \cite{A14}, Theorem 11.5.9. 1.99/1.64 This system is of type 3 or smaller. 1.99/1.64 This system is deterministic. 1.99/1.64 System R transformed to V(R) + Emb. 1.99/1.64 This system is terminating. 1.99/1.64 Call external tool: 1.99/1.64 ./ttt2.sh 1.99/1.64 Input: 1.99/1.64 (VAR x) 1.99/1.64 (RULES 1.99/1.64 f(x) -> a 1.99/1.64 f(x) -> x 1.99/1.64 f(x) -> x 1.99/1.64 ) 1.99/1.64 1.99/1.64 Polynomial Interpretation Processor: 1.99/1.64 dimension: 1 1.99/1.64 interpretation: 1.99/1.64 [a] = 0, 1.99/1.65 1.99/1.65 [f](x0) = 2x0 + 5x0x0 + 1 1.99/1.65 orientation: 1.99/1.65 f(x) = 2x + 5x*x + 1 >= 0 = a() 1.99/1.65 1.99/1.65 f(x) = 2x + 5x*x + 1 >= x = x 1.99/1.65 problem: 1.99/1.65 1.99/1.65 Qed 1.99/1.65 All 0 critical pairs are joinable. 1.99/1.65 3.18/1.68 EOF