1.95/1.89	YES
1.95/1.89	
1.95/1.89	Proof:
1.95/1.89	This system is confluent.
1.95/1.89	By \cite{ALS94}, Theorem 4.1.
1.95/1.89	This system is of type 3 or smaller.
1.95/1.89	This system is strongly deterministic.
1.95/1.89	This system is quasi-decreasing.
1.95/1.90	By \cite{A14}, Theorem 11.5.9.
1.95/1.90	This system is of type 3 or smaller.
1.95/1.90	This system is deterministic.
1.95/1.90	System R transformed to V(R) + Emb.
1.95/1.90	This system is terminating.
1.95/1.90	Call external tool:
1.95/1.90	./ttt2.sh
1.95/1.90	Input:
1.95/1.90	(VAR z y x)
1.95/1.90	(RULES
1.95/1.90	  sub(z, 0) -> z
1.95/1.90	  sub(s(z), s(y)) -> sub(z, y)
1.95/1.90	  s(x) -> x
1.95/1.90	  sub(x, y) -> x
1.95/1.90	  sub(x, y) -> y
1.95/1.90	)
1.95/1.90	
1.95/1.90	 Matrix Interpretation Processor: dim=3
1.95/1.90	  
1.95/1.90	  interpretation:
1.95/1.90	               
1.95/1.90	   [s](x0) = x0
1.95/1.90	               ,
1.95/1.90	   
1.95/1.90	                             [0]
1.95/1.90	   [sub](x0, x1) = x0 + x1 + [1]
1.95/1.90	                             [1],
1.95/1.90	   
1.95/1.90	         [1]
1.95/1.90	   [0] = [0]
1.95/1.90	         [0]
1.95/1.90	  orientation:
1.95/1.90	                    [1]         
1.95/1.90	   sub(z,0()) = z + [1] >= z = z
1.95/1.90	                    [1]         
1.95/1.90	   
1.95/1.90	                            [0]            [0]           
1.95/1.90	   sub(s(z),s(y)) = y + z + [1] >= y + z + [1] = sub(z,y)
1.95/1.90	                            [1]            [1]           
1.95/1.90	   
1.95/1.90	                    
1.95/1.90	   s(x) = x >= x = x
1.95/1.90	                    
1.95/1.90	   
1.95/1.90	                      [0]         
1.95/1.90	   sub(x,y) = x + y + [1] >= x = x
1.95/1.90	                      [1]         
1.95/1.90	   
1.95/1.90	                      [0]         
1.95/1.90	   sub(x,y) = x + y + [1] >= y = y
1.95/1.90	                      [1]         
1.95/1.90	  problem:
1.95/1.90	   sub(s(z),s(y)) -> sub(z,y)
1.95/1.90	   s(x) -> x
1.95/1.90	   sub(x,y) -> x
1.95/1.90	   sub(x,y) -> y
1.95/1.90	  Matrix Interpretation Processor: dim=3
1.95/1.90	   
1.95/1.90	   interpretation:
1.95/1.90	                
1.95/1.90	    [s](x0) = x0
1.95/1.90	                ,
1.95/1.90	    
1.95/1.90	                         [1 1 0]     [1]
1.95/1.90	    [sub](x0, x1) = x0 + [0 1 1]x1 + [0]
1.95/1.90	                         [0 0 1]     [1]
1.95/1.90	   orientation:
1.95/1.90	                     [1 1 0]        [1]    [1 1 0]        [1]           
1.95/1.90	    sub(s(z),s(y)) = [0 1 1]y + z + [0] >= [0 1 1]y + z + [0] = sub(z,y)
1.95/1.90	                     [0 0 1]        [1]    [0 0 1]        [1]           
1.95/1.90	    
1.95/1.90	                     
1.95/1.90	    s(x) = x >= x = x
1.95/1.90	                     
1.95/1.90	    
1.95/1.90	                   [1 1 0]    [1]         
1.95/1.90	    sub(x,y) = x + [0 1 1]y + [0] >= x = x
4.22/1.91	                   [0 0 1]    [1]         
4.22/1.91	    
4.22/1.91	                   [1 1 0]    [1]         
4.22/1.91	    sub(x,y) = x + [0 1 1]y + [0] >= y = y
4.22/1.91	                   [0 0 1]    [1]         
4.22/1.91	   problem:
4.22/1.91	    sub(s(z),s(y)) -> sub(z,y)
4.22/1.91	    s(x) -> x
4.22/1.91	   Matrix Interpretation Processor: dim=3
4.22/1.91	    
4.22/1.91	    interpretation:
4.22/1.91	                    [0]
4.22/1.91	     [s](x0) = x0 + [0]
4.22/1.91	                    [1],
4.22/1.91	     
4.22/1.91	                     [1 0 0]     [1 0 1]  
4.22/1.91	     [sub](x0, x1) = [0 0 0]x0 + [0 0 0]x1
4.22/1.91	                     [0 0 0]     [0 0 0]  
4.22/1.91	    orientation:
4.22/1.91	                      [1 0 1]    [1 0 0]    [1]    [1 0 1]    [1 0 0]            
4.22/1.91	     sub(s(z),s(y)) = [0 0 0]y + [0 0 0]z + [0] >= [0 0 0]y + [0 0 0]z = sub(z,y)
4.22/1.91	                      [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]            
4.22/1.91	     
4.22/1.91	                [0]         
4.22/1.91	     s(x) = x + [0] >= x = x
4.22/1.91	                [1]         
4.22/1.91	    problem:
4.22/1.91	     s(x) -> x
4.22/1.91	    Matrix Interpretation Processor: dim=3
4.22/1.91	     
4.22/1.91	     interpretation:
4.22/1.91	                     [1]
4.22/1.91	      [s](x0) = x0 + [0]
4.22/1.91	                     [0]
4.22/1.91	     orientation:
4.22/1.91	                 [1]         
4.22/1.91	      s(x) = x + [0] >= x = x
4.22/1.91	                 [0]         
4.22/1.91	     problem:
4.22/1.91	      
4.22/1.91	     Qed
4.22/1.91	All 0 critical pairs are joinable.
4.22/1.91	
4.22/1.93	EOF