2.20/1.10 YES 2.20/1.10 2.20/1.10 Problem: 2.20/1.10 even(0()) -> true() 2.20/1.10 even(s(x)) -> true() <= odd(x) = true() 2.20/1.10 odd(s(x)) -> true() <= even(x) = true() 2.20/1.10 2.20/1.10 Proof: 2.20/1.10 This system is confluent. 2.20/1.10 By \cite{ALS94}, Theorem 4.1. 2.20/1.10 This system is of type 3 or smaller. 2.20/1.10 This system is strongly deterministic. 2.20/1.10 All 0 critical pairs are joinable. 2.20/1.10 This system is quasi-decreasing. 2.20/1.10 By \cite{A14}, Theorem 11.5.9. 2.20/1.10 This system is of type 3 or smaller. 2.20/1.10 This system is deterministic. 2.20/1.10 System R transformed to V(R) + Emb. 2.20/1.10 This system is terminating. 2.20/1.10 Call external tool: 2.20/1.10 ./ttt2.sh 2.20/1.10 Input: 2.20/1.10 even(0()) -> true() 2.20/1.10 even(s(x)) -> true() 2.20/1.10 even(s(x)) -> odd(x) 2.20/1.10 odd(s(x)) -> true() 2.20/1.10 odd(s(x)) -> even(x) 2.20/1.10 even(x) -> x 2.20/1.10 s(x) -> x 2.20/1.10 odd(x) -> x 2.20/1.10 2.20/1.10 Matrix Interpretation Processor: dim=3 2.20/1.10 2.20/1.10 interpretation: 2.20/1.10 2.20/1.10 [odd](x0) = x0 2.20/1.10 , 2.20/1.10 2.20/1.10 [1] 2.20/1.10 [s](x0) = x0 + [0] 2.20/1.10 [0], 2.20/1.10 2.20/1.10 [0] 2.20/1.10 [true] = [0] 2.20/1.10 [0], 2.20/1.10 2.20/1.10 2.20/1.10 [even](x0) = x0 2.20/1.10 , 2.20/1.10 2.20/1.10 [1] 2.20/1.10 [0] = [0] 2.20/1.10 [0] 2.20/1.10 orientation: 2.20/1.11 [1] [0] 2.20/1.11 even(0()) = [0] >= [0] = true() 2.20/1.11 [0] [0] 2.20/1.11 2.20/1.11 [1] [0] 2.20/1.11 even(s(x)) = x + [0] >= [0] = true() 2.20/1.11 [0] [0] 2.20/1.11 2.20/1.11 [1] 2.20/1.11 even(s(x)) = x + [0] >= x = odd(x) 2.20/1.11 [0] 2.20/1.11 2.20/1.11 [1] [0] 2.20/1.11 odd(s(x)) = x + [0] >= [0] = true() 2.20/1.11 [0] [0] 2.20/1.11 2.20/1.11 [1] 2.20/1.11 odd(s(x)) = x + [0] >= x = even(x) 2.20/1.11 [0] 2.20/1.11 2.20/1.11 2.20/1.11 even(x) = x >= x = x 2.20/1.11 2.20/1.11 2.20/1.11 [1] 2.20/1.11 s(x) = x + [0] >= x = x 2.20/1.11 [0] 2.20/1.11 2.20/1.11 2.20/1.11 odd(x) = x >= x = x 2.20/1.11 2.20/1.11 problem: 2.20/1.11 even(x) -> x 2.20/1.11 odd(x) -> x 2.20/1.11 Matrix Interpretation Processor: dim=3 2.20/1.11 2.20/1.11 interpretation: 2.20/1.11 [1] 2.20/1.11 [odd](x0) = x0 + [0] 2.20/1.11 [0], 2.20/1.11 2.20/1.11 2.20/1.11 [even](x0) = x0 2.20/1.11 2.20/1.11 orientation: 2.20/1.11 2.20/1.11 even(x) = x >= x = x 2.20/1.11 2.20/1.11 2.20/1.11 [1] 2.20/1.11 odd(x) = x + [0] >= x = x 2.20/1.11 [0] 2.20/1.11 problem: 2.20/1.11 even(x) -> x 2.20/1.11 Matrix Interpretation Processor: dim=3 2.20/1.11 2.20/1.11 interpretation: 2.20/1.11 [1] 2.20/1.11 [even](x0) = x0 + [0] 2.20/1.11 [0] 2.20/1.11 orientation: 2.20/1.11 [1] 2.20/1.11 even(x) = x + [0] >= x = x 2.20/1.11 [0] 2.20/1.11 problem: 2.20/1.11 2.20/1.11 Qed 2.20/1.11 2.93/1.28 EOF