4.60/2.06	YES
4.60/2.06	
4.60/2.06	Proof:
4.60/2.06	This system is confluent.
4.60/2.06	By \cite{ALS94}, Theorem 4.1.
4.60/2.06	This system is of type 3 or smaller.
4.60/2.06	This system is strongly deterministic.
4.60/2.06	This system is quasi-decreasing.
4.60/2.06	By \cite{A14}, Theorem 11.5.9.
4.60/2.06	This system is of type 3 or smaller.
4.60/2.06	This system is deterministic.
4.60/2.06	System R transformed to V(R) + Emb.
4.60/2.06	This system is terminating.
4.60/2.06	Call external tool:
4.60/2.06	./ttt2.sh
4.60/2.06	Input:
4.60/2.06	(VAR x)
4.60/2.06	(RULES
4.60/2.06	  f(x) -> a
4.60/2.06	  f(x) -> b
4.60/2.06	  f(x) -> x
4.60/2.06	)
4.60/2.06	
4.60/2.06	 Polynomial Interpretation Processor:
4.60/2.06	  dimension: 1
4.60/2.06	  interpretation:
4.60/2.06	   [b] = 0,
4.60/2.06	   
4.60/2.06	   [a] = 0,
4.60/2.06	   
4.60/2.06	   [f](x0) = 4x0 + 1
4.60/2.06	  orientation:
4.60/2.06	   f(x) = 4x + 1 >= 0 = a()
4.60/2.06	   
4.60/2.06	   f(x) = 4x + 1 >= 0 = b()
4.60/2.06	   
4.60/2.06	   f(x) = 4x + 1 >= x = x
4.60/2.06	  problem:
4.60/2.06	   
4.60/2.06	  Qed
4.60/2.06	All 2 critical pairs are joinable.
4.60/2.06	Overlap: (rule1: f(y) -> b <= b = y, rule2: f(z) -> a <= a = z, pos: ε, mgu: {(y,z)})
4.60/2.06	CP: a = b <= b = z, a = z
4.60/2.06	This critical pair is context-joinable.
4.60/2.06	Overlap: (rule1: f(y) -> a <= a = y, rule2: f(z) -> b <= b = z, pos: ε, mgu: {(y,z)})
4.60/2.06	CP: b = a <= a = z, b = z
4.60/2.06	This critical pair is context-joinable.
4.60/2.06	
4.72/2.10	EOF