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