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