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