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