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