3.10/1.34	YES
3.10/1.34	
3.10/1.34	Proof:
3.10/1.34	This system is confluent.
3.10/1.34	By \cite{ALS94}, Theorem 4.1.
3.10/1.34	This system is of type 3 or smaller.
3.10/1.34	This system is strongly deterministic.
3.10/1.34	This system is quasi-decreasing.
3.10/1.34	By \cite{O02}, p. 214, Proposition 7.2.50.
3.10/1.34	This system is of type 3 or smaller.
3.10/1.34	This system is deterministic.
3.10/1.34	System R transformed to optimized U(R).
3.10/1.34	This system is terminating.
3.10/1.34	Call external tool:
3.10/1.34	./ttt2.sh
3.10/1.34	Input:
3.10/1.34	  add(x, 0) -> x
3.10/1.34	  add(x, s(y)) -> s(add(x, y))
3.10/1.34	  quad(x) -> ?1(add(x, x), x)
3.10/1.34	  ?1(y, x) -> ?2(add(y, y), x, y)
3.10/1.34	  ?2(z, x, y) -> z
3.10/1.34	
3.10/1.34	 Matrix Interpretation Processor: dim=1
3.10/1.34	  
3.10/1.34	  interpretation:
3.10/1.34	   [?2](x0, x1, x2) = x0 + x1 + x2,
3.10/1.34	   
3.10/1.34	   [?1](x0, x1) = 3x0 + x1 + 1,
3.10/1.34	   
3.10/1.34	   [quad](x0) = 7x0 + 1,
3.10/1.34	   
3.10/1.34	   [s](x0) = x0,
3.10/1.34	   
3.10/1.34	   [add](x0, x1) = x0 + x1,
3.10/1.34	   
3.10/1.34	   [0] = 0
3.10/1.34	  orientation:
3.10/1.34	   add(x,0()) = x >= x = x
3.10/1.34	   
3.10/1.34	   add(x,s(y)) = x + y >= x + y = s(add(x,y))
3.10/1.34	   
3.10/1.34	   quad(x) = 7x + 1 >= 7x + 1 = ?1(add(x,x),x)
3.10/1.34	   
3.10/1.34	   ?1(y,x) = x + 3y + 1 >= x + 3y = ?2(add(y,y),x,y)
3.10/1.34	   
3.10/1.34	   ?2(z,x,y) = x + y + z >= z = z
3.10/1.34	  problem:
3.10/1.34	   add(x,0()) -> x
3.10/1.34	   add(x,s(y)) -> s(add(x,y))
3.10/1.34	   quad(x) -> ?1(add(x,x),x)
3.10/1.34	   ?2(z,x,y) -> z
3.10/1.34	  Matrix Interpretation Processor: dim=1
3.10/1.34	   
3.10/1.34	   interpretation:
3.10/1.34	    [?2](x0, x1, x2) = 4x0 + x1 + x2,
3.10/1.34	    
3.10/1.34	    [?1](x0, x1) = x0 + x1,
3.10/1.34	    
3.10/1.34	    [quad](x0) = 7x0 + 4,
3.10/1.34	    
3.10/1.34	    [s](x0) = x0 + 4,
3.10/1.34	    
3.10/1.34	    [add](x0, x1) = 2x0 + 4x1,
3.10/1.34	    
3.10/1.34	    [0] = 1
3.10/1.34	   orientation:
3.10/1.34	    add(x,0()) = 2x + 4 >= x = x
3.10/1.34	    
3.10/1.34	    add(x,s(y)) = 2x + 4y + 16 >= 2x + 4y + 4 = s(add(x,y))
3.10/1.34	    
3.10/1.34	    quad(x) = 7x + 4 >= 7x = ?1(add(x,x),x)
3.10/1.34	    
3.10/1.34	    ?2(z,x,y) = x + y + 4z >= z = z
3.10/1.34	   problem:
3.10/1.34	    ?2(z,x,y) -> z
3.10/1.34	   Matrix Interpretation Processor: dim=3
3.10/1.34	    
3.10/1.34	    interpretation:
3.10/1.34	                             [1 0 0]     [1 0 0]     [1]
3.10/1.34	     [?2](x0, x1, x2) = x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
3.10/1.35	                             [0 0 0]     [0 0 0]     [0]
3.10/1.35	    orientation:
3.10/1.35	                 [1 0 0]    [1 0 0]        [1]         
3.10/1.35	     ?2(z,x,y) = [0 0 0]x + [0 0 0]y + z + [0] >= z = z
3.10/1.35	                 [0 0 0]    [0 0 0]        [0]         
3.10/1.35	    problem:
3.10/1.35	     
3.10/1.35	    Qed
3.10/1.35	All 0 critical pairs are joinable.
3.10/1.35	
3.21/1.38	EOF