11.16/3.35	YES
11.16/3.35	
11.16/3.35	Problem:
11.16/3.35	even(0()) -> true()
11.16/3.35	even(s(x)) -> false() <= odd(x) = false()
11.16/3.35	even(s(x)) -> true() <= odd(x) = true()
11.16/3.35	odd(0()) -> false()
11.16/3.35	odd(s(x)) -> false() <= even(x) = false()
11.16/3.35	odd(s(x)) -> true() <= even(x) = true()
11.16/3.35	
11.16/3.35	Proof:
11.16/3.35	This system is confluent.
11.16/3.35	By \cite{ALS94}, Theorem 4.1.
11.16/3.35	This system is of type 3 or smaller.
11.16/3.35	This system is strongly deterministic.
11.16/3.35	All 4 critical pairs are joinable.
11.16/3.35	CP: false() = true() <= odd(x) = true(), odd(x) = false():
11.16/3.35	This critical pair is unfeasible.
11.16/3.35	CP: true() = false() <= odd(x) = false(), odd(x) = true():
11.16/3.35	This critical pair is unfeasible.
11.16/3.35	CP: false() = true() <= even(x) = true(), even(x) = false():
11.16/3.35	This critical pair is unfeasible.
11.16/3.35	CP: true() = false() <= even(x) = false(), even(x) = true():
11.16/3.35	This critical pair is unfeasible.
11.16/3.35	This system is quasi-decreasing.
11.16/3.35	By \cite{O02}, p. 214, Proposition 7.2.50.
11.16/3.35	This system is of type 3 or smaller.
11.16/3.35	This system is deterministic.
11.16/3.35	System R transformed to U(R).
11.16/3.35	This system is terminating.
11.16/3.35	Call external tool:
11.16/3.35	./ttt2.sh
11.16/3.35	Input:
11.16/3.35	  even(0()) -> true()
11.16/3.35	  ?1(false(), x) -> false()
11.16/3.35	  even(s(x)) -> ?1(odd(x), x)
11.16/3.35	  ?2(true(), x) -> true()
11.16/3.35	  even(s(x)) -> ?2(odd(x), x)
11.16/3.35	  odd(0()) -> false()
11.16/3.35	  ?3(false(), x) -> false()
11.16/3.35	  odd(s(x)) -> ?3(even(x), x)
11.16/3.35	  ?4(true(), x) -> true()
11.16/3.35	  odd(s(x)) -> ?4(even(x), x)
11.16/3.35	
11.16/3.35	 Matrix Interpretation Processor: dim=1
11.16/3.35	  
11.16/3.35	  interpretation:
11.16/3.35	   [?4](x0, x1) = 4x0 + 2x1 + 7,
11.16/3.35	   
11.16/3.35	   [?3](x0, x1) = x0 + 2x1 + 1,
11.16/3.35	   
11.16/3.35	   [?2](x0, x1) = 2x0 + 2x1 + 2,
11.16/3.35	   
11.16/3.35	   [odd](x0) = 5x0 + 3,
11.16/3.35	   
11.16/3.35	   [s](x0) = 4x0 + 4,
11.16/3.36	   
11.16/3.36	   [?1](x0, x1) = x0 + x1 + 6,
11.16/3.36	   
11.16/3.36	   [false] = 2,
11.16/3.36	   
11.16/3.36	   [true] = 2,
11.16/3.36	   
11.16/3.36	   [even](x0) = 4x0 + 4,
11.16/3.36	   
11.16/3.36	   [0] = 2
11.16/3.36	  orientation:
11.16/3.36	   even(0()) = 12 >= 2 = true()
11.16/3.36	   
11.16/3.36	   ?1(false(),x) = x + 8 >= 2 = false()
11.16/3.36	   
11.16/3.36	   even(s(x)) = 16x + 20 >= 6x + 9 = ?1(odd(x),x)
11.16/3.36	   
11.16/3.36	   ?2(true(),x) = 2x + 6 >= 2 = true()
11.16/3.36	   
11.16/3.36	   even(s(x)) = 16x + 20 >= 12x + 8 = ?2(odd(x),x)
11.16/3.36	   
11.16/3.37	   odd(0()) = 13 >= 2 = false()
11.16/3.38	   
11.16/3.38	   ?3(false(),x) = 2x + 3 >= 2 = false()
11.16/3.38	   
11.16/3.38	   odd(s(x)) = 20x + 23 >= 6x + 5 = ?3(even(x),x)
11.16/3.38	   
11.16/3.38	   ?4(true(),x) = 2x + 15 >= 2 = true()
11.16/3.38	   
11.16/3.38	   odd(s(x)) = 20x + 23 >= 18x + 23 = ?4(even(x),x)
11.16/3.38	  problem:
11.16/3.38	   odd(s(x)) -> ?4(even(x),x)
11.16/3.38	  Matrix Interpretation Processor: dim=3
11.16/3.38	   
11.16/3.38	   interpretation:
11.16/3.38	                   [1 1 0]     [1 0 0]  
11.16/3.38	    [?4](x0, x1) = [0 0 0]x0 + [0 0 0]x1
11.16/3.38	                   [0 0 0]     [0 0 0]  ,
11.16/3.38	    
11.16/3.38	                [1 1 1]     [1]
11.16/3.38	    [odd](x0) = [0 0 0]x0 + [0]
11.16/3.38	                [0 0 0]     [0],
11.16/3.38	    
11.16/3.38	              [1 0 0]  
11.16/3.38	    [s](x0) = [1 0 0]x0
11.16/3.38	              [1 0 0]  ,
11.16/3.38	    
11.16/3.38	                 [1 0 0]  
11.16/3.38	    [even](x0) = [1 0 0]x0
11.16/3.38	                 [0 0 0]  
11.16/3.38	   orientation:
11.16/3.38	                [3 0 0]    [1]    [3 0 0]                 
11.16/3.38	    odd(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?4(even(x),x)
11.16/3.38	                [0 0 0]    [0]    [0 0 0]                 
11.16/3.38	   problem:
11.16/3.38	    
11.16/3.38	   Qed
11.16/3.38	
12.55/3.75	EOF