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