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