3.61/1.77	YES
3.61/1.77	
3.61/1.77	Proof:
3.61/1.77	This system is confluent.
3.61/1.77	By \cite{ALS94}, Theorem 4.1.
3.61/1.77	This system is of type 3 or smaller.
3.61/1.77	This system is strongly deterministic.
3.61/1.77	This system is quasi-decreasing.
3.61/1.77	By \cite{O02}, p. 214, Proposition 7.2.50.
3.61/1.77	This system is of type 3 or smaller.
3.61/1.77	This system is deterministic.
3.61/1.77	System R transformed to optimized U(R).
3.61/1.77	This system is terminating.
3.61/1.77	Call external tool:
3.61/1.77	./ttt2.sh
3.61/1.77	Input:
3.61/1.77	(VAR x x' y x'')
3.61/1.77	(RULES
3.61/1.77	  f(x, x') -> ?1(x, x, x')
3.61/1.77	  ?1(y, x, x') -> ?2(x', x, x', y)
3.61/1.77	  ?2(y, x, x', y) -> g(y, y)
3.61/1.77	  h(x, x', x'') -> ?3(x, x, x', x'')
3.61/1.77	  ?3(y, x, x', x'') -> ?4(x', x, x', x'', y)
3.61/1.77	  ?4(y, x, x', x'', y) -> ?5(x'', x, x', x'', y)
3.61/1.77	  ?5(y, x, x', x'', y) -> c
3.61/1.77	)
3.61/1.77	
3.61/1.77	 Polynomial Interpretation Processor:
3.61/1.77	  dimension: 1
3.61/1.77	  interpretation:
3.61/1.77	   [c] = 0,
3.61/1.77	   
3.61/1.77	   [?5](x0, x1, x2, x3, x4) = x1 + x3 + x4 + x0x0 + x1x1 + 2x2x2 + x3x3 + 1,
3.61/1.77	   
3.61/1.77	   [?4](x0, x1, x2, x3, x4) = x1 + 2x2 + 2x3 + 2x4 + x0x0 + x1x1 + 2x2x2 + 3x3x3 + 4,
3.61/1.77	   
3.61/1.77	   [?3](x0, x1, x2, x3) = 2x0 + x1 + 2x2 + 2x3 + x1x1 + 3x2x2 + 3x3x3 + 6,
3.61/1.77	   
3.61/1.77	   [h](x0, x1, x2) = 3x0 + 4x1 + 2x2 + 6x0x0 + 3x1x1 + 3x2x2 + 7,
3.61/1.77	   
3.61/1.77	   [g](x0, x1) = 4x0 + x1,
3.61/1.77	   
3.61/1.77	   [?2](x0, x1, x2, x3) = x0 + 3x2 + 4x3 + 7x0x0 + x1x1 + 2,
3.61/1.77	   
3.61/1.78	   [?1](x0, x1, x2) = 4x0 + 2x1 + 4x2 + x0x0 + x1x1 + 7x2x2 + 4,
3.61/1.78	   
3.61/1.78	   [f](x0, x1) = 7x0 + 4x1 + 4x0x0 + 7x1x1 + 5
3.61/1.78	  orientation:
3.61/1.78	   f(x,x') = 7x + 4x*x + 4x' + 7x'*x' + 5 >= 6x + 2x*x + 4x' + 7x'*x' + 4 = ?1(x,x,x')
3.61/1.78	   
3.61/1.78	   ?1(y,x,x') = 2x + x*x + 4x' + 7x'*x' + 4y + y*y + 4 >= x*x + 4x' + 7x'*x' + 4y + 2 = ?2(x',x,x',y)
3.61/1.78	   
3.61/1.78	   ?2(y,x,x',y) = x*x + 3x' + 5y + 7y*y + 2 >= 5y = g(y,y)
3.61/1.78	   
3.61/1.78	   h(x,x',x'') = 3x + 6x*x + 4x' + 3x'*x' + 2x'' + 3x''*x'' + 7 >= 3x + x*x + 2x' + 3x'*x' + 2x'' + 3x''*x'' + 6 = ?3(x,x,x',x'')
3.61/1.78	   
3.61/1.78	   ?3(y,x,x',x'') = x + x*x + 2x' + 3x'*x' + 2x'' + 3x''*x'' + 2y + 6 >= x + x*x + 2x' + 3x'*x' + 2x'' + 3x''*x'' + 2y + 4 = ?4(x',x,x',x'',y)
3.61/1.78	   
3.61/1.78	   ?4(y,x,x',x'',y) = x + x*x + 2x' + 2x'*x' + 2x'' + 3x''*x'' + 2y + y*y + 4 >= x + x*x + 2x'*x' + x'' + 2x''*x'' + y + 1 = ?5(x'',x,x',x'',y)
3.61/1.78	   
3.61/1.78	   ?5(y,x,x',x'',y) = x + x*x + 2x'*x' + x'' + x''*x'' + y + y*y + 1 >= 0 = c()
3.61/1.78	  problem:
3.61/1.78	   
3.61/1.78	  Qed
3.61/1.78	All 0 critical pairs are joinable.
3.61/1.78	
3.61/1.78	EOF