6.55/2.16	YES
6.55/2.16	
6.55/2.16	Problem:
6.55/2.16	f(x', x'') -> g(x) <= x' = x, x'' = x
6.55/2.16	f(y', h(y'')) -> g(y) <= y' = y, y'' = y
6.55/2.16	
6.55/2.16	Proof:
6.55/2.16	This system is confluent.
6.55/2.16	By \cite{ALS94}, Theorem 4.1.
6.55/2.16	This system is of type 3 or smaller.
6.55/2.16	This system is strongly deterministic.
6.55/2.16	All 2 critical pairs are joinable.
6.55/2.16	CP: g(y') = g(z') <= $1 = z', $2 = z', $1 = y', h($2) = y':
6.55/2.16	This critical pair is infeasible.
6.55/2.16	This critical pair is conditional.
6.55/2.16	This critical pair has some non-trivial conditions.
6.55/2.16	usable rules
6.55/2.16	'\Sigma(h($2)) \cap (->^*_R)[\Sigma(REN(y'))]' is empty.
6.55/2.16	CP: g(x') = g(y') <= $1 = y', h($2) = y', $1 = x', $2 = x':
6.55/2.16	This critical pair is infeasible.
6.55/2.16	This critical pair is conditional.
6.55/2.16	This critical pair has some non-trivial conditions.
6.55/2.16	usable rules
6.55/2.16	'\Sigma(h($2)) \cap (->^*_R)[\Sigma(REN(y'))]' is empty.
6.55/2.16	This system is quasi-decreasing.
6.55/2.16	By \cite{O02}, p. 214, Proposition 7.2.50.
6.55/2.16	This system is of type 3 or smaller.
6.55/2.16	This system is deterministic.
6.55/2.16	System R transformed to U(R).
6.55/2.16	This system is terminating.
6.55/2.16	Call external tool:
6.55/2.16	./ttt2.sh
6.55/2.16	Input:
6.55/2.16	  ?2(x, x', x'', x) -> g(x)
6.55/2.16	  ?1(x, x', x'') -> ?2(x'', x', x'', x)
6.55/2.16	  f(x', x'') -> ?1(x', x', x'')
6.55/2.16	  ?4(y, y', y'', y) -> g(y)
6.55/2.16	  ?3(y, y', y'') -> ?4(y'', y', y'', y)
6.55/2.16	  f(y', h(y'')) -> ?3(y', y', y'')
6.55/2.16	
6.55/2.16	 Polynomial Interpretation Processor:
6.55/2.16	  dimension: 1
6.55/2.16	  interpretation:
6.55/2.16	   [h](x0) = x0,
6.55/2.16	   
6.55/2.16	   [?3](x0, x1, x2) = -2x0 + 5x2 + 5x0x0 + x1x1 + 3x2x2 + 3,
6.55/2.16	   
6.55/2.16	   [?4](x0, x1, x2, x3) = 2x0 + 2x2 + -3x3 + x1x1 + 2x2x2 + 4x3x3 + 2,
6.55/2.16	   
6.55/2.16	   [f](x0, x1) = x0 + 5x1 + 6x0x0 + 4x1x1 + 5,
6.55/2.16	   
6.55/2.16	   [?1](x0, x1, x2) = 5x2 + x0x0 + 4x1x1 + 4x2x2 + 3,
6.55/2.16	   
6.55/2.16	   [g](x0) = -1x0 + 2x0x0,
6.55/2.16	   
6.55/2.16	   [?2](x0, x1, x2, x3) = 5x2 + x0x0 + 2x1x1 + 3x2x2 + x3x3 + 2
6.55/2.16	  orientation:
6.55/2.16	   ?2(x,x',x'',x) = 2x*x + 2x'*x' + 5x'' + 3x''*x'' + 2 >= -1x + 2x*x = g(x)
6.55/2.16	   
6.55/2.16	   ?1(x,x',x'') = x*x + 4x'*x' + 5x'' + 4x''*x'' + 3 >= x*x + 2x'*x' + 5x'' + 4x''*x'' + 2 = ?2(x'',x',x'',x)
6.55/2.16	   
6.55/2.16	   f(x',x'') = x' + 6x'*x' + 5x'' + 4x''*x'' + 5 >= 5x'*x' + 5x'' + 4x''*x'' + 3 = ?1(x',x',x'')
6.55/2.16	   
6.55/2.16	   ?4(y,y',y'',y) = -1y + 4y*y + y'*y' + 2y'' + 2y''*y'' + 2 >= -1y + 2y*y = g(y)
6.55/2.16	   
6.55/2.16	   ?3(y,y',y'') = -2y + 5y*y + y'*y' + 5y'' + 3y''*y'' + 3 >= -3y + 4y*y + y'*y' + 4y'' + 2y''*y'' + 2 = ?4(y'',y',y'',y)
6.55/2.16	   
6.55/2.16	   f(y',h(y'')) = y' + 6y'*y' + 5y'' + 4y''*y'' + 5 >= -2y' + 6y'*y' + 5y'' + 3y''*y'' + 3 = ?3(y',y',y'')
6.55/2.16	  problem:
6.55/2.16	   
6.55/2.16	  Qed
6.55/2.16	
7.41/2.36	EOF