3.74/1.90	YES
3.74/1.90	
3.74/1.90	Proof:
3.74/1.90	This system is confluent.
3.74/1.90	By \cite{ALS94}, Theorem 4.1.
3.74/1.90	This system is of type 3 or smaller.
3.74/1.90	This system is strongly deterministic.
3.74/1.90	This system is quasi-decreasing.
3.74/1.90	By \cite{O02}, p. 214, Proposition 7.2.50.
3.74/1.91	This system is of type 3 or smaller.
3.74/1.91	This system is deterministic.
3.74/1.91	System R transformed to U(R).
3.74/1.91	This system is terminating.
3.74/1.91	Call external tool:
3.74/1.91	./ttt2.sh
3.74/1.91	Input:
3.74/1.91	(VAR x)
3.74/1.91	(RULES
3.74/1.91	  even(0) -> true
3.74/1.91	  ?1(true, x) -> true
3.74/1.91	  even(s(x)) -> ?1(odd(x), x)
3.74/1.91	  ?2(true, x) -> true
3.74/1.91	  odd(s(x)) -> ?2(even(x), x)
3.74/1.91	)
3.74/1.91	
3.74/1.91	 Matrix Interpretation Processor: dim=3
3.74/1.91	  
3.74/1.91	  interpretation:
3.74/1.91	                  [1 0 0]     [1 0 0]  
3.74/1.91	   [?2](x0, x1) = [0 1 0]x0 + [0 0 1]x1
3.74/1.91	                  [0 0 0]     [0 0 0]  ,
3.74/1.91	   
3.74/1.91	               [1 0 1]     [1]
3.74/1.91	   [odd](x0) = [1 0 0]x0 + [0]
3.74/1.91	               [0 0 0]     [0],
3.74/1.91	   
3.74/1.91	             [1 0 1]     [0]
3.74/1.91	   [s](x0) = [1 0 0]x0 + [0]
3.74/1.91	             [1 1 0]     [1],
3.74/1.91	   
3.74/1.91	                  [1 1 0]     [1 0 0]  
3.74/1.91	   [?1](x0, x1) = [0 1 0]x0 + [0 0 1]x1
3.74/1.91	                  [1 1 0]     [0 1 0]  ,
3.74/1.91	   
3.74/1.91	            [0]
3.74/1.91	   [true] = [1]
3.74/1.91	            [0],
3.74/1.91	   
3.74/1.91	                [1 1 1]  
3.77/1.91	   [even](x0) = [1 0 0]x0
3.77/1.91	                [1 0 1]  ,
3.77/1.91	   
3.77/1.91	         [1]
3.77/1.91	   [0] = [1]
3.77/1.91	         [0]
3.77/1.91	  orientation:
3.77/1.91	               [2]    [0]         
3.77/1.91	   even(0()) = [1] >= [1] = true()
3.77/1.91	               [1]    [0]         
3.77/1.91	   
3.77/1.91	                  [1 0 0]    [1]    [0]         
3.77/1.91	   ?1(true(),x) = [0 0 1]x + [1] >= [1] = true()
3.77/1.91	                  [0 1 0]    [1]    [0]         
3.77/1.91	   
3.77/1.91	                [3 1 1]    [1]    [3 0 1]    [1]               
3.77/1.91	   even(s(x)) = [1 0 1]x + [0] >= [1 0 1]x + [0] = ?1(odd(x),x)
3.77/1.91	                [2 1 1]    [1]    [2 1 1]    [1]               
3.77/1.91	   
3.77/1.91	                  [1 0 0]    [0]    [0]         
3.77/1.91	   ?2(true(),x) = [0 0 1]x + [1] >= [1] = true()
3.77/1.91	                  [0 0 0]    [0]    [0]         
3.77/1.92	   
3.77/1.92	               [2 1 1]    [2]    [2 1 1]                 
3.77/1.92	   odd(s(x)) = [1 0 1]x + [0] >= [1 0 1]x = ?2(even(x),x)
3.77/1.92	               [0 0 0]    [0]    [0 0 0]                 
3.77/1.92	  problem:
3.77/1.92	   even(s(x)) -> ?1(odd(x),x)
3.77/1.92	   ?2(true(),x) -> true()
3.77/1.92	  Matrix Interpretation Processor: dim=1
3.77/1.92	   
3.77/1.92	   interpretation:
3.77/1.92	    [?2](x0, x1) = x0 + 4x1,
3.77/1.92	    
3.77/1.92	    [odd](x0) = x0,
3.77/1.92	    
3.77/1.92	    [s](x0) = x0 + 4,
3.77/1.92	    
3.77/1.92	    [?1](x0, x1) = x0 + x1,
3.77/1.92	    
3.77/1.92	    [true] = 1,
3.77/1.92	    
3.77/1.92	    [even](x0) = 4x0
3.77/1.92	   orientation:
3.77/1.92	    even(s(x)) = 4x + 16 >= 2x = ?1(odd(x),x)
3.77/1.92	    
3.77/1.92	    ?2(true(),x) = 4x + 1 >= 1 = true()
3.77/1.92	   problem:
3.77/1.92	    ?2(true(),x) -> true()
3.77/1.92	   Matrix Interpretation Processor: dim=3
3.77/1.92	    
3.77/1.92	    interpretation:
3.77/1.92	                    [1 1 0]     [1 0 0]     [0]
3.77/1.92	     [?2](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
3.77/1.92	                    [0 0 0]     [0 0 0]     [0],
3.77/1.92	     
3.77/1.92	              [0]
3.77/1.92	     [true] = [1]
3.77/1.92	              [0]
3.77/1.92	    orientation:
3.77/1.92	                    [1 0 0]    [1]    [0]         
3.77/1.92	     ?2(true(),x) = [0 0 0]x + [1] >= [1] = true()
3.77/1.92	                    [0 0 0]    [0]    [0]         
3.77/1.92	    problem:
3.77/1.92	     
3.77/1.92	    Qed
3.77/1.92	All 0 critical pairs are joinable.
3.77/1.92	
4.22/1.95	EOF