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