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