2.95/1.72	YES
2.95/1.72	
2.95/1.72	Proof:
2.95/1.72	This system is confluent.
2.95/1.72	By \cite{ALS94}, Theorem 4.1.
2.95/1.72	This system is of type 3 or smaller.
2.95/1.72	This system is strongly deterministic.
2.95/1.72	This system is quasi-decreasing.
2.95/1.72	By \cite{A14}, Theorem 11.5.9.
2.95/1.72	This system is of type 3 or smaller.
2.95/1.72	This system is deterministic.
2.95/1.72	System R transformed to V(R) + Emb.
2.95/1.72	This system is terminating.
2.95/1.72	Call external tool:
2.95/1.72	./ttt2.sh
2.95/1.72	Input:
2.95/1.72	(VAR x y)
2.95/1.72	(RULES
2.95/1.72	  a -> b
2.95/1.72	  f(x) -> A
2.95/1.72	  f(x) -> x
2.95/1.72	  g(x, x) -> h(x)
2.95/1.72	  h(x) -> i(x)
2.95/1.72	  h(x) -> x
2.95/1.72	  g(x, y) -> x
2.95/1.72	  g(x, y) -> y
2.95/1.72	  f(x) -> x
2.95/1.72	  i(x) -> x
2.95/1.72	)
2.95/1.72	
2.95/1.72	 Polynomial Interpretation Processor:
2.95/1.72	  dimension: 1
2.95/1.72	  interpretation:
2.95/1.72	   [i](x0) = 2x0 + 2x0x0 + 4,
2.95/1.72	   
2.95/1.72	   [h](x0) = 2x0 + 7x0x0 + 6,
2.95/1.72	   
2.95/1.72	   [g](x0, x1) = 7x0 + 4x1 + 7x1x1 + 7,
2.95/1.72	   
2.95/1.72	   [A] = 0,
2.95/1.72	   
2.95/1.72	   [f](x0) = 2x0 + 1,
2.95/1.72	   
2.95/1.72	   [b] = 0,
2.95/1.72	   
2.95/1.72	   [a] = 2
2.95/1.72	  orientation:
2.95/1.72	   a() = 2 >= 0 = b()
2.95/1.72	   
2.95/1.72	   f(x) = 2x + 1 >= 0 = A()
2.95/1.72	   
2.95/1.72	   f(x) = 2x + 1 >= x = x
2.95/1.72	   
2.95/1.72	   g(x,x) = 11x + 7x*x + 7 >= 2x + 7x*x + 6 = h(x)
2.95/1.72	   
2.95/1.72	   h(x) = 2x + 7x*x + 6 >= 2x + 2x*x + 4 = i(x)
2.95/1.72	   
2.95/1.72	   h(x) = 2x + 7x*x + 6 >= x = x
2.95/1.72	   
2.95/1.72	   g(x,y) = 7x + 4y + 7y*y + 7 >= x = x
2.95/1.72	   
2.95/1.72	   g(x,y) = 7x + 4y + 7y*y + 7 >= y = y
2.95/1.72	   
2.95/1.72	   i(x) = 2x + 2x*x + 4 >= x = x
2.95/1.72	  problem:
2.95/1.72	   
2.95/1.72	  Qed
2.95/1.72	All 0 critical pairs are joinable.
2.95/1.72	
3.34/1.77	EOF