1.29/1.09	YES
1.29/1.09	
1.29/1.09	Proof:
1.29/1.09	This system is confluent.
1.29/1.09	By \cite{ALS94}, Theorem 4.1.
1.29/1.09	This system is of type 3 or smaller.
1.29/1.09	This system is strongly deterministic.
1.29/1.09	This system is quasi-decreasing.
1.29/1.09	By \cite{O02}, p. 214, Proposition 7.2.50.
1.29/1.09	This system is of type 3 or smaller.
1.29/1.09	This system is deterministic.
1.29/1.09	System R transformed to U(R).
1.29/1.09	This system is terminating.
1.29/1.09	Call external tool:
1.29/1.09	./ttt2.sh
1.29/1.09	Input:
1.29/1.09	  f(x) -> x
1.29/1.09	  ?1(b, x) -> a
1.29/1.09	  g(x) -> ?1(x, x)
1.29/1.09	
1.29/1.09	 Polynomial Interpretation Processor:
1.29/1.09	  dimension: 1
1.29/1.09	  interpretation:
1.29/1.09	   [g](x0) = 4x0 + 5x0x0 + 4,
1.29/1.09	   
1.29/1.09	   [a] = 0,
1.29/1.09	   
1.29/1.09	   [?1](x0, x1) = -2x0 + 4x0x0 + x1x1 + 1,
1.29/1.09	   
1.29/1.09	   [b] = 2,
1.29/1.09	   
1.29/1.09	   [f](x0) = x0 + 4
1.29/1.09	  orientation:
1.29/1.09	   f(x) = x + 4 >= x = x
1.29/1.09	   
1.29/1.09	   ?1(b(),x) = x*x + 13 >= 0 = a()
1.29/1.09	   
1.29/1.09	   g(x) = 4x + 5x*x + 4 >= -2x + 5x*x + 1 = ?1(x,x)
1.29/1.09	  problem:
1.29/1.09	   
1.29/1.09	  Qed
1.29/1.09	All 0 critical pairs are joinable.
1.29/1.09	
2.28/1.12	EOF