6.22/2.51	YES
6.22/2.51	
6.22/2.51	Proof:
6.22/2.52	This system is confluent.
6.22/2.52	By \cite{ALS94}, Theorem 4.1.
6.22/2.52	This system is of type 3 or smaller.
6.22/2.52	This system is strongly deterministic.
6.22/2.52	This system is quasi-decreasing.
6.22/2.52	By \cite{O02}, p. 214, Proposition 7.2.50.
6.22/2.52	This system is of type 3 or smaller.
6.22/2.52	This system is deterministic.
6.22/2.52	System R transformed to optimized U(R).
6.22/2.52	This system is terminating.
6.22/2.52	Call external tool:
6.22/2.52	./ttt2.sh
6.22/2.52	Input:
6.22/2.52	(VAR x y)
6.22/2.52	(RULES
6.22/2.52	  f(x, y) -> ?1(c(g(x)), x, y)
6.22/2.52	  ?1(c(a), x, y) -> g(x)
6.22/2.52	  f(x, y) -> ?2(c(h(x)), x, y)
6.22/2.52	  ?2(c(a), x, y) -> h(x)
6.22/2.52	  g(s(x)) -> x
6.22/2.52	  h(s(x)) -> x
6.22/2.52	)
6.22/2.52	
6.22/2.52	 Matrix Interpretation Processor: dim=1
6.22/2.52	  
6.22/2.52	  interpretation:
6.22/2.52	   [s](x0) = 2x0 + 4,
6.22/2.52	   
6.22/2.52	   [?2](x0, x1, x2) = 2x0 + 4x1 + x2,
6.22/2.52	   
6.22/2.52	   [h](x0) = x0,
6.22/2.52	   
6.22/2.52	   [a] = 1,
6.22/2.52	   
6.22/2.52	   [?1](x0, x1, x2) = x0 + x1 + 2x2,
6.22/2.52	   
6.22/2.52	   [c](x0) = x0,
6.22/2.52	   
6.22/2.52	   [g](x0) = x0 + 1,
6.22/2.52	   
6.22/2.52	   [f](x0, x1) = 6x0 + 3x1 + 1
6.22/2.52	  orientation:
6.22/2.52	   f(x,y) = 6x + 3y + 1 >= 2x + 2y + 1 = ?1(c(g(x)),x,y)
6.22/2.52	   
6.22/2.52	   ?1(c(a()),x,y) = x + 2y + 1 >= x + 1 = g(x)
6.22/2.52	   
6.22/2.52	   f(x,y) = 6x + 3y + 1 >= 6x + y = ?2(c(h(x)),x,y)
6.22/2.52	   
6.22/2.52	   ?2(c(a()),x,y) = 4x + y + 2 >= x = h(x)
6.22/2.53	   
6.22/2.53	   g(s(x)) = 2x + 5 >= x = x
6.22/2.53	   
6.22/2.53	   h(s(x)) = 2x + 4 >= x = x
6.22/2.53	  problem:
6.22/2.53	   f(x,y) -> ?1(c(g(x)),x,y)
6.22/2.53	   ?1(c(a()),x,y) -> g(x)
6.22/2.53	  Matrix Interpretation Processor: dim=1
6.22/2.53	   
6.22/2.53	   interpretation:
6.22/2.53	    [a] = 0,
6.22/2.53	    
6.22/2.53	    [?1](x0, x1, x2) = x0 + x1 + x2,
6.22/2.53	    
6.22/2.53	    [c](x0) = x0 + 6,
6.22/2.53	    
6.22/2.53	    [g](x0) = x0,
6.22/2.53	    
6.22/2.53	    [f](x0, x1) = 3x0 + x1 + 6
6.22/2.53	   orientation:
6.22/2.53	    f(x,y) = 3x + y + 6 >= 2x + y + 6 = ?1(c(g(x)),x,y)
6.22/2.53	    
6.22/2.53	    ?1(c(a()),x,y) = x + y + 6 >= x = g(x)
6.22/2.53	   problem:
6.22/2.53	    f(x,y) -> ?1(c(g(x)),x,y)
6.22/2.53	   Matrix Interpretation Processor: dim=1
6.22/2.53	    
6.22/2.53	    interpretation:
6.22/2.53	     [?1](x0, x1, x2) = 3x0 + x1 + 4x2,
6.22/2.53	     
6.22/2.53	     [c](x0) = x0,
6.22/2.53	     
6.22/2.53	     [g](x0) = 2x0,
6.22/2.53	     
6.22/2.53	     [f](x0, x1) = 7x0 + 4x1 + 1
6.22/2.53	    orientation:
6.22/2.53	     f(x,y) = 7x + 4y + 1 >= 7x + 4y = ?1(c(g(x)),x,y)
6.22/2.53	    problem:
6.22/2.53	     
6.22/2.53	    Qed
6.22/2.53	All 2 critical pairs are joinable.
6.22/2.53	Overlap: (rule1: f(z, x') -> h(z) <= c(h(z)) = c(a), rule2: f(y', z') -> g(y') <= c(g(y')) = c(a), pos: ε, mgu: {(z,y'), (x',z')})
6.22/2.53	CP: g(y') = h(y') <= c(h(y')) = c(a), c(g(y')) = c(a)
6.22/2.53	This critical pair is infeasible.
6.22/2.53	This critical pair is conditional.
6.22/2.53	This critical pair has some non-trivial conditions.
6.22/2.53	Call external tool:
6.22/2.53	./waldmeister
6.22/2.53	Input:
6.22/2.53	  f(x, y) -> g(x) <= c(g(x)) = c(a)
6.22/2.53	  f(x, y) -> h(x) <= c(h(x)) = c(a)
6.22/2.53	  g(s(x)) -> x
6.22/2.53	  h(s(x)) -> x
6.22/2.53	
6.22/2.53	By Waldmeister.
6.22/2.53	Overlap: (rule1: f(z, x') -> g(z) <= c(g(z)) = c(a), rule2: f(y', z') -> h(y') <= c(h(y')) = c(a), pos: ε, mgu: {(z,y'), (x',z')})
6.22/2.53	CP: h(y') = g(y') <= c(g(y')) = c(a), c(h(y')) = c(a)
6.22/2.53	This critical pair is infeasible.
6.22/2.53	This critical pair is conditional.
6.22/2.53	This critical pair has some non-trivial conditions.
6.22/2.53	Call external tool:
6.22/2.53	./waldmeister
6.22/2.53	Input:
6.22/2.53	  f(x, y) -> g(x) <= c(g(x)) = c(a)
6.22/2.53	  f(x, y) -> h(x) <= c(h(x)) = c(a)
6.22/2.53	  g(s(x)) -> x
6.22/2.53	  h(s(x)) -> x
6.22/2.53	
6.22/2.53	By Waldmeister.
6.22/2.54	
6.41/2.56	EOF