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