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