2.15/1.15	YES
2.15/1.15	
2.15/1.15	Proof:
2.38/1.15	This system is confluent.
2.38/1.15	By \cite{ALS94}, Theorem 4.1.
2.38/1.15	This system is of type 3 or smaller.
2.38/1.15	This system is strongly deterministic.
2.38/1.15	This system is quasi-decreasing.
2.38/1.15	By \cite{A14}, Theorem 11.5.9.
2.38/1.15	This system is of type 3 or smaller.
2.38/1.15	This system is deterministic.
2.38/1.15	System R transformed to V(R) + Emb.
2.38/1.15	This system is terminating.
2.38/1.15	Call external tool:
2.38/1.15	./ttt2.sh
2.38/1.15	Input:
2.38/1.15	  f(x, x) -> a
2.38/1.15	  f(x, x) -> g(x)
2.38/1.15	  g(x) -> x
2.38/1.15	  f(x, y) -> x
2.38/1.15	  f(x, y) -> y
2.38/1.15	
2.38/1.15	 Polynomial Interpretation Processor:
2.38/1.15	  dimension: 1
2.38/1.15	  interpretation:
2.38/1.15	   [g](x0) = 4x0 + 2x0x0 + 4,
2.38/1.15	   
2.38/1.15	   [a] = 0,
2.38/1.15	   
2.38/1.15	   [f](x0, x1) = 4x0 + x1 + 2x1x1 + 5
2.38/1.15	  orientation:
2.38/1.15	   f(x,x) = 5x + 2x*x + 5 >= 0 = a()
2.38/1.15	   
2.38/1.15	   f(x,x) = 5x + 2x*x + 5 >= 4x + 2x*x + 4 = g(x)
2.38/1.15	   
2.38/1.15	   g(x) = 4x + 2x*x + 4 >= x = x
2.38/1.15	   
2.38/1.15	   f(x,y) = 4x + y + 2y*y + 5 >= x = x
2.38/1.15	   
2.38/1.15	   f(x,y) = 4x + y + 2y*y + 5 >= y = y
2.38/1.15	  problem:
2.38/1.15	   
2.38/1.15	  Qed
2.38/1.16	All 0 critical pairs are joinable.
2.38/1.16	
2.72/1.23	EOF