11.02/3.42	YES
11.02/3.42	
11.02/3.42	Problem:
11.02/3.42	even(0()) -> true()
11.02/3.42	even(s(x)) -> false() <= odd(x) = false()
11.02/3.42	even(s(x)) -> true() <= odd(x) = true()
11.02/3.42	odd(0()) -> false()
11.02/3.42	odd(s(x)) -> false() <= even(x) = false()
11.02/3.42	odd(s(x)) -> true() <= even(x) = true()
11.02/3.42	
11.02/3.42	Proof:
11.02/3.42	This system is confluent.
11.02/3.42	By \cite{SMI95}, Corollary 4.7 or 5.3.
11.02/3.42	This system is oriented.
11.02/3.42	This system is of type 3 or smaller.
11.02/3.42	This system is right-stable.
11.02/3.42	This system is properly oriented.
11.02/3.42	This is an overlay system.
11.02/3.42	This system is left-linear.
11.02/3.42	All 4 critical pairs are trivial or infeasible.
11.02/3.42	CP: false() = true() <= odd(x) = true(), odd(x) = false():
11.02/3.42	This critical pair is infeasible.
11.02/3.42	This critical pair is conditional.
11.02/3.42	This critical pair has some non-trivial conditions.
11.02/3.42	This system is of type 3 or smaller.
11.02/3.42	This system is deterministic.
11.02/3.42	This system is quasi-decreasing.
11.02/3.42	By \cite{O02}, p. 214, Proposition 7.2.50.
11.02/3.42	This system is of type 3 or smaller.
11.02/3.42	This system is deterministic.
11.02/3.42	System R transformed to optimized U(R).
11.02/3.42	This system is terminating.
11.02/3.42	Call external tool:
11.02/3.42	./ttt2.sh
11.02/3.42	Input:
11.02/3.42	  even(0()) -> true()
11.02/3.42	  ?1(false(), x) -> false()
11.02/3.42	  even(s(x)) -> ?1(odd(x), x)
11.02/3.42	  ?1(true(), x) -> true()
11.02/3.42	  odd(0()) -> false()
11.02/3.42	  ?2(false(), x) -> false()
11.02/3.42	  odd(s(x)) -> ?2(even(x), x)
11.02/3.42	  ?2(true(), x) -> true()
11.02/3.42	
11.02/3.42	 Matrix Interpretation Processor: dim=3
11.02/3.42	  
11.02/3.42	  interpretation:
11.02/3.42	                  [1 1 0]     [1 1 0]  
11.02/3.42	   [?2](x0, x1) = [1 1 0]x0 + [0 0 0]x1
11.02/3.42	                  [0 1 0]     [0 1 0]  ,
11.02/3.42	   
11.02/3.42	               [1 0 1]     [1]
11.02/3.42	   [odd](x0) = [0 1 1]x0 + [0]
11.02/3.42	               [0 0 1]     [0],
11.02/3.42	   
11.02/3.42	             [1 1 1]     [0]
11.02/3.42	   [s](x0) = [0 0 1]x0 + [1]
11.02/3.42	             [1 1 1]     [0],
11.02/3.42	   
11.02/3.42	                  [1 1 0]     [1 0 0]     [0]
11.02/3.42	   [?1](x0, x1) = [0 1 0]x0 + [0 0 0]x1 + [0]
11.02/3.42	                  [0 1 1]     [1 0 0]     [1],
11.02/3.42	   
11.02/3.42	             [1]
11.02/3.42	   [false] = [1]
11.02/3.42	             [1],
11.02/3.42	   
11.02/3.42	            [0]
11.02/3.42	   [true] = [1]
11.02/3.42	            [0],
11.02/3.42	   
11.02/3.42	                [1 0 1]     [1]
11.02/3.42	   [even](x0) = [0 0 1]x0 + [0]
11.02/3.42	                [1 1 0]     [0],
11.02/3.42	   
11.02/3.42	         [0]
11.02/3.42	   [0] = [0]
11.02/3.42	         [1]
11.02/3.42	  orientation:
11.02/3.42	               [2]    [0]         
11.02/3.42	   even(0()) = [1] >= [1] = true()
11.02/3.42	               [0]    [0]         
11.02/3.42	   
11.02/3.42	                   [1 0 0]    [2]    [1]          
11.02/3.42	   ?1(false(),x) = [0 0 0]x + [1] >= [1] = false()
11.02/3.42	                   [1 0 0]    [3]    [1]          
11.02/3.42	   
11.02/3.42	                [2 2 2]    [1]    [2 1 2]    [1]               
11.02/3.42	   even(s(x)) = [1 1 1]x + [0] >= [0 1 1]x + [0] = ?1(odd(x),x)
11.02/3.42	                [1 1 2]    [1]    [1 1 2]    [1]               
11.02/3.42	   
11.02/3.42	                  [1 0 0]    [1]    [0]         
11.02/3.42	   ?1(true(),x) = [0 0 0]x + [1] >= [1] = true()
11.02/3.42	                  [1 0 0]    [2]    [0]         
11.02/3.42	   
11.02/3.42	              [2]    [1]          
11.02/3.42	   odd(0()) = [1] >= [1] = false()
11.02/3.42	              [1]    [1]          
11.02/3.42	   
11.02/3.42	                   [1 1 0]    [2]    [1]          
11.02/3.42	   ?2(false(),x) = [0 0 0]x + [2] >= [1] = false()
11.02/3.42	                   [0 1 0]    [1]    [1]          
11.02/3.42	   
11.02/3.42	               [2 2 2]    [1]    [2 1 2]    [1]                
11.02/3.42	   odd(s(x)) = [1 1 2]x + [1] >= [1 0 2]x + [1] = ?2(even(x),x)
11.02/3.42	               [1 1 1]    [0]    [0 1 1]    [0]                
11.02/3.42	   
11.02/3.42	                  [1 1 0]    [1]    [0]         
11.02/3.42	   ?2(true(),x) = [0 0 0]x + [1] >= [1] = true()
11.02/3.42	                  [0 1 0]    [1]    [0]         
11.02/3.42	  problem:
11.02/3.42	   even(s(x)) -> ?1(odd(x),x)
11.02/3.42	   odd(s(x)) -> ?2(even(x),x)
11.02/3.42	  Matrix Interpretation Processor: dim=1
11.02/3.42	   
11.02/3.42	   interpretation:
11.02/3.42	    [?2](x0, x1) = 2x0 + 4x1,
11.02/3.42	    
11.02/3.42	    [odd](x0) = x0 + 4,
11.02/3.42	    
11.02/3.42	    [s](x0) = 6x0 + 7,
11.02/3.42	    
11.02/3.42	    [?1](x0, x1) = 3x0 + 3x1,
11.02/3.42	    
11.02/3.42	    [even](x0) = x0 + 5
11.02/3.42	   orientation:
11.02/3.42	    even(s(x)) = 6x + 12 >= 6x + 12 = ?1(odd(x),x)
11.02/3.42	    
11.02/3.42	    odd(s(x)) = 6x + 11 >= 6x + 10 = ?2(even(x),x)
11.02/3.42	   problem:
11.02/3.42	    even(s(x)) -> ?1(odd(x),x)
11.02/3.42	   Matrix Interpretation Processor: dim=3
11.02/3.42	    
11.02/3.42	    interpretation:
11.02/3.42	                 [1 0 0]  
11.02/3.42	     [odd](x0) = [1 0 0]x0
11.02/3.42	                 [0 0 0]  ,
11.02/3.42	     
11.02/3.42	               [1 0 0]  
11.02/3.42	     [s](x0) = [1 0 0]x0
11.02/3.42	               [1 0 0]  ,
11.02/3.42	     
11.02/3.42	                    [1 1 0]     [1 0 0]  
11.02/3.42	     [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1
11.02/3.42	                    [0 0 0]     [0 0 0]  ,
11.02/3.42	     
11.02/3.42	                  [1 1 1]     [1]
11.02/3.42	     [even](x0) = [0 0 0]x0 + [0]
11.02/3.42	                  [0 0 0]     [0]
11.02/3.42	    orientation:
11.02/3.43	                  [3 0 0]    [1]    [3 0 0]                
11.02/3.43	     even(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?1(odd(x),x)
11.02/3.43	                  [0 0 0]    [0]    [0 0 0]                
11.02/3.43	    problem:
11.02/3.43	     
11.02/3.43	    Qed
11.02/3.43	This critical pair is unfeasible.
11.02/3.43	CP: true() = false() <= odd(x) = false(), odd(x) = true():
11.02/3.43	This critical pair is infeasible.
11.02/3.43	This critical pair is conditional.
11.02/3.43	This critical pair has some non-trivial conditions.
11.02/3.43	This system is of type 3 or smaller.
11.02/3.43	This system is deterministic.
11.02/3.43	This system is quasi-decreasing.
11.02/3.43	By \cite{A14}, Theorem 11.5.9.
11.02/3.43	This system is of type 3 or smaller.
11.02/3.43	This system is deterministic.
11.02/3.43	System R transformed to V(R) + Emb.
11.02/3.43	This system is terminating.
11.02/3.43	Call external tool:
11.02/3.43	./ttt2.sh
11.02/3.43	Input:
11.02/3.43	  even(0()) -> true()
11.02/3.43	  even(s(x)) -> false()
11.02/3.43	  even(s(x)) -> odd(x)
11.02/3.43	  even(s(x)) -> true()
11.02/3.43	  odd(0()) -> false()
11.02/3.43	  odd(s(x)) -> false()
11.02/3.43	  odd(s(x)) -> even(x)
11.02/3.43	  odd(s(x)) -> true()
11.02/3.43	  even(x) -> x
11.02/3.43	  s(x) -> x
11.02/3.43	  odd(x) -> x
11.02/3.43	
11.02/3.43	 Matrix Interpretation Processor: dim=3
11.02/3.43	  
11.02/3.43	  interpretation:
11.02/3.43	                 
11.02/3.43	   [odd](x0) = x0
11.02/3.43	                 ,
11.02/3.43	   
11.02/3.43	             [0]
11.02/3.43	   [false] = [0]
11.02/3.43	             [0],
11.02/3.43	   
11.02/3.43	                  [1]
11.02/3.43	   [s](x0) = x0 + [0]
11.02/3.43	                  [0],
11.02/3.43	   
11.02/3.43	            [0]
11.02/3.43	   [true] = [0]
11.02/3.43	            [0],
11.02/3.43	   
11.02/3.43	                  
11.02/3.43	   [even](x0) = x0
11.02/3.43	                  ,
11.02/3.43	   
11.02/3.43	         [1]
11.02/3.43	   [0] = [0]
11.02/3.43	         [0]
11.02/3.43	  orientation:
11.02/3.43	               [1]    [0]         
11.02/3.43	   even(0()) = [0] >= [0] = true()
11.02/3.43	               [0]    [0]         
11.02/3.43	   
11.02/3.43	                    [1]    [0]          
11.02/3.43	   even(s(x)) = x + [0] >= [0] = false()
11.02/3.43	                    [0]    [0]          
11.02/3.43	   
11.02/3.43	                    [1]              
11.02/3.43	   even(s(x)) = x + [0] >= x = odd(x)
11.02/3.43	                    [0]              
11.02/3.43	   
11.02/3.43	                    [1]    [0]         
11.02/3.43	   even(s(x)) = x + [0] >= [0] = true()
11.02/3.43	                    [0]    [0]         
11.02/3.43	   
11.02/3.43	              [1]    [0]          
11.02/3.43	   odd(0()) = [0] >= [0] = false()
11.02/3.43	              [0]    [0]          
11.02/3.43	   
11.02/3.43	                   [1]    [0]          
11.02/3.43	   odd(s(x)) = x + [0] >= [0] = false()
11.02/3.43	                   [0]    [0]          
11.02/3.43	   
11.02/3.43	                   [1]               
11.02/3.43	   odd(s(x)) = x + [0] >= x = even(x)
11.02/3.43	                   [0]               
11.02/3.43	   
11.02/3.43	                   [1]    [0]         
11.02/3.43	   odd(s(x)) = x + [0] >= [0] = true()
11.02/3.43	                   [0]    [0]         
11.02/3.43	   
11.02/3.43	                       
11.02/3.43	   even(x) = x >= x = x
11.02/3.43	                       
11.02/3.43	   
11.02/3.43	              [1]         
11.02/3.43	   s(x) = x + [0] >= x = x
11.02/3.43	              [0]         
11.02/3.43	   
11.02/3.43	                      
11.02/3.43	   odd(x) = x >= x = x
11.02/3.43	                      
11.02/3.43	  problem:
11.02/3.43	   even(x) -> x
11.02/3.43	   odd(x) -> x
11.02/3.43	  Matrix Interpretation Processor: dim=3
11.02/3.43	   
11.02/3.43	   interpretation:
11.02/3.43	                     [1]
11.02/3.43	    [odd](x0) = x0 + [0]
11.02/3.43	                     [0],
11.02/3.43	    
11.02/3.43	                   
11.02/3.43	    [even](x0) = x0
11.02/3.43	                   
11.02/3.43	   orientation:
11.02/3.44	                        
11.02/3.44	    even(x) = x >= x = x
11.02/3.44	                        
11.02/3.44	    
11.02/3.44	                 [1]         
11.02/3.44	    odd(x) = x + [0] >= x = x
11.02/3.44	                 [0]         
11.02/3.44	   problem:
11.02/3.44	    even(x) -> x
11.02/3.44	   Matrix Interpretation Processor: dim=3
11.02/3.44	    
11.02/3.44	    interpretation:
11.02/3.44	                       [1]
11.02/3.44	     [even](x0) = x0 + [0]
11.02/3.44	                       [0]
11.02/3.44	    orientation:
11.02/3.44	                   [1]         
11.02/3.44	     even(x) = x + [0] >= x = x
11.02/3.44	                   [0]         
11.02/3.44	    problem:
11.02/3.44	     
11.02/3.44	    Qed
11.02/3.44	This critical pair is unfeasible.
11.02/3.44	CP: false() = true() <= even(x) = true(), even(x) = false():
11.02/3.44	This critical pair is infeasible.
11.02/3.44	This critical pair is conditional.
11.02/3.44	This critical pair has some non-trivial conditions.
11.02/3.44	This system is of type 3 or smaller.
11.02/3.44	This system is deterministic.
11.02/3.44	This system is quasi-decreasing.
11.02/3.44	By \cite{O02}, p. 214, Proposition 7.2.50.
11.02/3.44	This system is of type 3 or smaller.
11.02/3.44	This system is deterministic.
11.02/3.44	System R transformed to U(R).
11.02/3.44	This system is terminating.
11.02/3.44	Call external tool:
11.02/3.44	./ttt2.sh
11.02/3.44	Input:
11.02/3.44	  even(0()) -> true()
11.02/3.44	  ?1(false(), x) -> false()
11.02/3.44	  even(s(x)) -> ?1(odd(x), x)
11.02/3.44	  ?2(true(), x) -> true()
11.02/3.44	  even(s(x)) -> ?2(odd(x), x)
11.02/3.44	  odd(0()) -> false()
11.02/3.44	  ?3(false(), x) -> false()
11.02/3.44	  odd(s(x)) -> ?3(even(x), x)
11.02/3.44	  ?4(true(), x) -> true()
11.02/3.44	  odd(s(x)) -> ?4(even(x), x)
11.02/3.44	
11.02/3.44	 Matrix Interpretation Processor: dim=1
11.02/3.44	  
11.02/3.44	  interpretation:
11.02/3.44	   [?4](x0, x1) = 4x0 + 2x1 + 7,
11.02/3.44	   
11.02/3.44	   [?3](x0, x1) = x0 + 2x1 + 1,
11.02/3.44	   
11.02/3.44	   [?2](x0, x1) = 2x0 + 2x1 + 2,
11.02/3.44	   
11.02/3.44	   [odd](x0) = 5x0 + 3,
11.02/3.44	   
11.02/3.44	   [s](x0) = 4x0 + 4,
11.02/3.44	   
11.02/3.44	   [?1](x0, x1) = x0 + x1 + 6,
11.02/3.44	   
11.02/3.44	   [false] = 2,
11.02/3.44	   
11.02/3.44	   [true] = 2,
11.02/3.44	   
11.02/3.44	   [even](x0) = 4x0 + 4,
11.02/3.44	   
11.02/3.44	   [0] = 2
11.02/3.44	  orientation:
11.02/3.44	   even(0()) = 12 >= 2 = true()
11.02/3.44	   
11.02/3.44	   ?1(false(),x) = x + 8 >= 2 = false()
11.02/3.44	   
11.02/3.44	   even(s(x)) = 16x + 20 >= 6x + 9 = ?1(odd(x),x)
11.02/3.44	   
11.02/3.44	   ?2(true(),x) = 2x + 6 >= 2 = true()
11.02/3.44	   
11.02/3.44	   even(s(x)) = 16x + 20 >= 12x + 8 = ?2(odd(x),x)
11.02/3.44	   
11.02/3.44	   odd(0()) = 13 >= 2 = false()
11.02/3.44	   
11.02/3.44	   ?3(false(),x) = 2x + 3 >= 2 = false()
11.02/3.44	   
11.02/3.44	   odd(s(x)) = 20x + 23 >= 6x + 5 = ?3(even(x),x)
11.02/3.44	   
11.02/3.44	   ?4(true(),x) = 2x + 15 >= 2 = true()
11.02/3.44	   
11.02/3.44	   odd(s(x)) = 20x + 23 >= 18x + 23 = ?4(even(x),x)
11.02/3.44	  problem:
11.02/3.44	   odd(s(x)) -> ?4(even(x),x)
11.02/3.44	  Matrix Interpretation Processor: dim=3
11.02/3.44	   
11.02/3.44	   interpretation:
11.02/3.44	                   [1 1 0]     [1 0 0]  
11.02/3.44	    [?4](x0, x1) = [0 0 0]x0 + [0 0 0]x1
11.02/3.44	                   [0 0 0]     [0 0 0]  ,
11.02/3.44	    
11.02/3.44	                [1 1 1]     [1]
11.02/3.44	    [odd](x0) = [0 0 0]x0 + [0]
11.02/3.44	                [0 0 0]     [0],
11.02/3.44	    
11.02/3.44	              [1 0 0]  
11.02/3.44	    [s](x0) = [1 0 0]x0
11.02/3.44	              [1 0 0]  ,
11.02/3.44	    
11.02/3.44	                 [1 0 0]  
11.02/3.44	    [even](x0) = [1 0 0]x0
11.02/3.44	                 [0 0 0]  
11.02/3.44	   orientation:
11.02/3.44	                [3 0 0]    [1]    [3 0 0]                 
11.02/3.44	    odd(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?4(even(x),x)
11.02/3.44	                [0 0 0]    [0]    [0 0 0]                 
11.02/3.44	   problem:
11.02/3.44	    
11.02/3.44	   Qed
11.02/3.44	This critical pair is unfeasible.
11.02/3.44	CP: true() = false() <= even(x) = false(), even(x) = true():
11.02/3.45	This critical pair is infeasible.
11.02/3.45	This critical pair is conditional.
11.02/3.45	This critical pair has some non-trivial conditions.
11.02/3.45	This system is of type 3 or smaller.
11.02/3.45	This system is deterministic.
11.02/3.45	This system is quasi-decreasing.
11.02/3.45	By \cite{O02}, p. 214, Proposition 7.2.50.
11.02/3.45	This system is of type 3 or smaller.
11.02/3.45	This system is deterministic.
11.02/3.45	System R transformed to U(R).
11.02/3.45	This system is terminating.
11.02/3.45	Call external tool:
11.02/3.45	./ttt2.sh
11.02/3.45	Input:
11.02/3.45	  even(0()) -> true()
11.02/3.45	  ?1(false(), x) -> false()
11.02/3.45	  even(s(x)) -> ?1(odd(x), x)
11.02/3.45	  ?2(true(), x) -> true()
11.02/3.45	  even(s(x)) -> ?2(odd(x), x)
11.02/3.45	  odd(0()) -> false()
11.02/3.45	  ?3(false(), x) -> false()
11.02/3.45	  odd(s(x)) -> ?3(even(x), x)
11.02/3.45	  ?4(true(), x) -> true()
11.02/3.45	  odd(s(x)) -> ?4(even(x), x)
11.02/3.45	
11.02/3.45	 Matrix Interpretation Processor: dim=1
11.02/3.45	  
11.02/3.45	  interpretation:
11.02/3.45	   [?4](x0, x1) = 4x0 + 2x1 + 7,
11.02/3.45	   
11.02/3.45	   [?3](x0, x1) = x0 + 2x1 + 1,
11.02/3.45	   
11.02/3.45	   [?2](x0, x1) = 2x0 + 2x1 + 2,
11.02/3.45	   
11.02/3.45	   [odd](x0) = 5x0 + 3,
11.02/3.45	   
11.02/3.45	   [s](x0) = 4x0 + 4,
11.02/3.45	   
11.02/3.45	   [?1](x0, x1) = x0 + x1 + 6,
11.02/3.45	   
11.02/3.45	   [false] = 2,
11.02/3.45	   
11.02/3.45	   [true] = 2,
11.02/3.45	   
11.02/3.45	   [even](x0) = 4x0 + 4,
11.02/3.45	   
11.02/3.45	   [0] = 2
11.02/3.45	  orientation:
11.02/3.45	   even(0()) = 12 >= 2 = true()
11.02/3.45	   
11.02/3.45	   ?1(false(),x) = x + 8 >= 2 = false()
11.02/3.45	   
11.02/3.45	   even(s(x)) = 16x + 20 >= 6x + 9 = ?1(odd(x),x)
11.02/3.45	   
11.02/3.45	   ?2(true(),x) = 2x + 6 >= 2 = true()
11.02/3.45	   
11.02/3.45	   even(s(x)) = 16x + 20 >= 12x + 8 = ?2(odd(x),x)
11.02/3.45	   
11.02/3.45	   odd(0()) = 13 >= 2 = false()
11.02/3.45	   
11.02/3.45	   ?3(false(),x) = 2x + 3 >= 2 = false()
11.02/3.45	   
11.02/3.45	   odd(s(x)) = 20x + 23 >= 6x + 5 = ?3(even(x),x)
11.02/3.45	   
11.02/3.45	   ?4(true(),x) = 2x + 15 >= 2 = true()
11.02/3.45	   
11.02/3.45	   odd(s(x)) = 20x + 23 >= 18x + 23 = ?4(even(x),x)
11.02/3.45	  problem:
11.02/3.45	   odd(s(x)) -> ?4(even(x),x)
11.02/3.45	  Matrix Interpretation Processor: dim=1
11.02/3.45	   
11.02/3.45	   interpretation:
11.02/3.45	    [?4](x0, x1) = 4x0 + 5x1,
11.02/3.45	    
11.02/3.45	    [odd](x0) = 5x0 + 7,
11.02/3.45	    
11.02/3.45	    [s](x0) = 6x0 + 4,
11.02/3.45	    
11.02/3.45	    [even](x0) = 6x0 + 4
11.02/3.45	   orientation:
11.02/3.45	    odd(s(x)) = 30x + 27 >= 29x + 16 = ?4(even(x),x)
11.02/3.45	   problem:
11.02/3.45	    
11.02/3.45	   Qed
11.02/3.45	This critical pair is unfeasible.
11.02/3.45	
11.02/3.47	EOF