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