3.87/1.90	YES
3.87/1.90	
3.87/1.90	Proof:
3.87/1.90	This system is confluent.
3.87/1.90	By \cite{ALS94}, Theorem 4.1.
3.87/1.90	This system is of type 3 or smaller.
3.87/1.90	This system is strongly deterministic.
3.87/1.90	This system is quasi-decreasing.
3.87/1.90	By \cite{A14}, Theorem 11.5.9.
3.87/1.90	This system is of type 3 or smaller.
3.87/1.90	This system is deterministic.
3.87/1.90	System R transformed to V(R) + Emb.
3.87/1.90	This system is terminating.
3.87/1.90	Call external tool:
3.87/1.90	./ttt2.sh
3.87/1.90	Input:
3.87/1.90	(VAR x)
3.87/1.90	(RULES
3.87/1.90	  f(x) -> a
3.87/1.90	  f(x) -> b
3.87/1.90	  f(x) -> x
3.87/1.90	)
3.87/1.90	
3.87/1.90	 Polynomial Interpretation Processor:
3.87/1.90	  dimension: 1
3.87/1.90	  interpretation:
3.87/1.90	   [b] = 0,
3.87/1.90	   
3.87/1.90	   [a] = 0,
3.87/1.90	   
3.87/1.90	   [f](x0) = 4x0 + 1
3.87/1.90	  orientation:
3.87/1.90	   f(x) = 4x + 1 >= 0 = a()
3.87/1.90	   
3.87/1.90	   f(x) = 4x + 1 >= 0 = b()
3.87/1.90	   
3.87/1.90	   f(x) = 4x + 1 >= x = x
3.87/1.90	  problem:
3.87/1.91	   
3.87/1.91	  Qed
3.87/1.91	All 2 critical pairs are joinable.
3.87/1.91	Overlap: (rule1: f(y) -> b <= b = y, rule2: f(z) -> a <= a = z, pos: ε, mgu: {(y,z)})
3.87/1.91	CP: a = b <= b = z, a = z
3.87/1.91	This critical pair is infeasible.
3.87/1.91	This critical pair is conditional.
3.87/1.91	This critical pair has some non-trivial conditions.
3.87/1.91	'tcap_{R_u}(conds(b, a))' and 'conds(z, z)' are not unifiable.
3.87/1.91	Overlap: (rule1: f(y) -> a <= a = y, rule2: f(z) -> b <= b = z, pos: ε, mgu: {(y,z)})
3.87/1.91	CP: b = a <= a = z, b = z
3.87/1.91	This critical pair is context-joinable.
3.87/1.91	
3.87/1.95	EOF