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