4.93/2.11	YES
4.93/2.11	
4.93/2.11	Proof:
4.93/2.11	This system is confluent.
4.93/2.11	Inlined conditions in System R.
4.93/2.11	By \cite{ALS94}, Theorem 4.1.
4.93/2.11	This system is of type 3 or smaller.
4.93/2.11	This system is strongly deterministic.
4.93/2.11	This system is quasi-decreasing.
4.93/2.11	By \cite{O02}, p. 214, Proposition 7.2.50.
4.93/2.11	This system is of type 3 or smaller.
4.93/2.11	This system is deterministic.
4.93/2.11	System R transformed to optimized U(R).
4.93/2.11	This system is terminating.
4.93/2.12	Call external tool:
4.93/2.12	./ttt2.sh
4.93/2.12	Input:
4.93/2.12	(VAR x y)
4.93/2.12	(RULES
4.93/2.12	  add(x, 0) -> x
4.93/2.12	  add(x, s(y)) -> s(add(x, y))
4.93/2.12	  quad(x) -> add(add(x, x), add(x, x))
4.93/2.12	)
4.93/2.12	
4.93/2.12	 Matrix Interpretation Processor: dim=1
4.93/2.12	  
4.93/2.12	  interpretation:
4.93/2.12	   [quad](x0) = 4x0 + 6,
4.93/2.12	   
4.93/2.12	   [s](x0) = x0,
4.93/2.12	   
4.93/2.12	   [add](x0, x1) = x0 + x1 + 2,
4.93/2.12	   
4.93/2.12	   [0] = 0
4.93/2.12	  orientation:
4.93/2.12	   add(x,0()) = x + 2 >= x = x
4.93/2.12	   
4.93/2.12	   add(x,s(y)) = x + y + 2 >= x + y + 2 = s(add(x,y))
4.93/2.12	   
4.93/2.12	   quad(x) = 4x + 6 >= 4x + 6 = add(add(x,x),add(x,x))
4.93/2.12	  problem:
4.93/2.12	   add(x,s(y)) -> s(add(x,y))
4.93/2.12	   quad(x) -> add(add(x,x),add(x,x))
4.93/2.12	  Matrix Interpretation Processor: dim=1
4.93/2.12	   
4.93/2.12	   interpretation:
4.93/2.12	    [quad](x0) = 4x0 + 1,
4.93/2.12	    
4.93/2.12	    [s](x0) = x0 + 2,
4.93/2.12	    
4.93/2.12	    [add](x0, x1) = x0 + x1
4.93/2.12	   orientation:
4.93/2.12	    add(x,s(y)) = x + y + 2 >= x + y + 2 = s(add(x,y))
4.93/2.12	    
4.93/2.12	    quad(x) = 4x + 1 >= 4x = add(add(x,x),add(x,x))
4.93/2.12	   problem:
4.93/2.12	    add(x,s(y)) -> s(add(x,y))
4.93/2.12	   Matrix Interpretation Processor: dim=3
4.93/2.12	    
4.93/2.12	    interpretation:
4.93/2.12	               [1 0 0]     [0]
4.93/2.12	     [s](x0) = [0 0 1]x0 + [0]
4.93/2.12	               [0 1 1]     [1],
4.93/2.12	     
4.93/2.12	                     [1 0 0]     [1 0 1]  
4.93/2.12	     [add](x0, x1) = [0 0 0]x0 + [0 1 0]x1
4.93/2.12	                     [0 0 0]     [0 0 1]  
4.93/2.12	    orientation:
4.93/2.12	                   [1 0 0]    [1 1 1]    [1]    [1 0 0]    [1 0 1]    [0]              
4.93/2.12	     add(x,s(y)) = [0 0 0]x + [0 0 1]y + [0] >= [0 0 0]x + [0 0 1]y + [0] = s(add(x,y))
4.93/2.12	                   [0 0 0]    [0 1 1]    [1]    [0 0 0]    [0 1 1]    [1]              
4.93/2.12	    problem:
4.93/2.12	     
4.93/2.12	    Qed
4.93/2.12	All 0 critical pairs are joinable.
4.93/2.12	
4.93/2.15	EOF