0.00/0.83 YES 0.00/0.83 0.00/0.83 Problem: 0.00/0.83 f(x, y) -> x <= g(x) = z, g(y) = z 0.00/0.83 g(x) -> c() <= d() = c() 0.00/0.83 0.00/0.83 Proof: 0.00/0.83 This system is confluent. 0.00/0.83 By \cite{ALS94}, Theorem 4.1. 0.00/0.83 This system is of type 3 or smaller. 0.00/0.83 This system is strongly deterministic. 0.00/0.83 All 0 critical pairs are joinable. 0.00/0.83 This system is quasi-decreasing. 0.00/0.83 By \cite{A14}, Theorem 11.5.9. 0.00/0.83 This system is of type 3 or smaller. 0.00/0.83 This system is deterministic. 0.00/0.83 System R transformed to V(R) + Emb. 0.00/0.83 This system is terminating. 0.00/0.83 Call external tool: 0.00/0.83 ./ttt2.sh 0.00/0.83 Input: 0.00/0.83 f(x, y) -> x 0.00/0.83 f(x, y) -> g(y) 0.00/0.83 f(x, y) -> g(x) 0.00/0.83 g(x) -> c() 0.00/0.83 g(x) -> d() 0.00/0.83 g(x) -> x 0.00/0.83 f(x, y) -> x 0.00/0.83 f(x, y) -> y 0.00/0.83 0.00/0.83 Polynomial Interpretation Processor: 0.00/0.83 dimension: 1 0.00/0.83 interpretation: 0.00/0.83 [d] = 0, 0.00/0.83 0.00/0.83 [c] = 0, 0.00/0.83 0.00/0.83 [g](x0) = 3x0 + 1, 0.00/0.83 0.00/0.83 [f](x0, x1) = 3x0 + 4x1 + 2 0.00/0.83 orientation: 0.00/0.83 f(x,y) = 3x + 4y + 2 >= x = x 0.00/0.83 0.00/0.83 f(x,y) = 3x + 4y + 2 >= 3y + 1 = g(y) 0.00/0.83 0.00/0.83 f(x,y) = 3x + 4y + 2 >= 3x + 1 = g(x) 0.00/0.83 0.00/0.83 g(x) = 3x + 1 >= 0 = c() 0.00/0.83 0.00/0.83 g(x) = 3x + 1 >= 0 = d() 0.00/0.83 0.00/0.83 g(x) = 3x + 1 >= x = x 0.00/0.83 0.00/0.83 f(x,y) = 3x + 4y + 2 >= y = y 0.00/0.83 problem: 0.00/0.83 0.00/0.83 Qed 0.00/0.83 0.00/0.89 EOF