1.99/1.70	YES
1.99/1.70	
1.99/1.70	Proof:
1.99/1.70	This system is confluent.
1.99/1.70	By \cite{ALS94}, Theorem 4.1.
1.99/1.70	This system is of type 3 or smaller.
1.99/1.70	This system is strongly deterministic.
1.99/1.70	This system is quasi-decreasing.
1.99/1.70	By \cite{O02}, p. 214, Proposition 7.2.50.
1.99/1.70	This system is of type 3 or smaller.
1.99/1.70	This system is deterministic.
1.99/1.70	System R transformed to optimized U(R).
1.99/1.70	This system is terminating.
1.99/1.70	Call external tool:
1.99/1.70	./ttt2.sh
1.99/1.70	Input:
1.99/1.70	(VAR x y)
1.99/1.70	(RULES
1.99/1.70	  f(x) -> ?1(x, x)
1.99/1.70	  ?1(a, x) -> x
1.99/1.70	  g(x) -> h(x, x)
1.99/1.70	  h(x, y) -> i(x)
1.99/1.70	)
1.99/1.70	
1.99/1.70	 Matrix Interpretation Processor: dim=1
1.99/1.70	  
1.99/1.70	  interpretation:
1.99/1.70	   [i](x0) = x0,
1.99/1.70	   
1.99/1.70	   [h](x0, x1) = x0 + 4x1 + 4,
1.99/1.70	   
1.99/1.70	   [g](x0) = 5x0 + 6,
1.99/1.70	   
1.99/1.70	   [a] = 4,
1.99/1.70	   
1.99/1.70	   [?1](x0, x1) = 4x0 + x1 + 1,
1.99/1.70	   
1.99/1.70	   [f](x0) = 5x0 + 4
1.99/1.70	  orientation:
1.99/1.70	   f(x) = 5x + 4 >= 5x + 1 = ?1(x,x)
1.99/1.70	   
1.99/1.70	   ?1(a(),x) = x + 17 >= x = x
1.99/1.70	   
1.99/1.70	   g(x) = 5x + 6 >= 5x + 4 = h(x,x)
1.99/1.70	   
1.99/1.70	   h(x,y) = x + 4y + 4 >= x = i(x)
1.99/1.70	  problem:
1.99/1.70	   
1.99/1.70	  Qed
1.99/1.70	All 0 critical pairs are joinable.
1.99/1.70	
3.28/1.73	EOF