4.79/2.44	YES
4.79/2.44	
4.79/2.44	Proof:
4.79/2.44	This system is confluent.
4.79/2.44	By \cite{ALS94}, Theorem 4.1.
4.79/2.44	This system is of type 3 or smaller.
4.79/2.44	This system is strongly deterministic.
4.79/2.44	This system is quasi-decreasing.
4.79/2.44	By \cite{O02}, p. 214, Proposition 7.2.50.
4.79/2.44	This system is of type 3 or smaller.
4.79/2.44	This system is deterministic.
4.79/2.44	System R transformed to optimized U(R).
4.79/2.44	This system is terminating.
4.79/2.44	Call external tool:
4.79/2.44	./ttt2.sh
4.79/2.44	Input:
4.79/2.44	  f(x, y) -> ?1(c(g(x)), x, y)
4.79/2.44	  ?1(c(a), x, y) -> g(s(x))
4.79/2.44	  f(x, y) -> ?2(c(h(x)), x, y)
4.79/2.44	  ?2(c(a), x, y) -> h(s(x))
4.79/2.44	  g(s(x)) -> x
4.79/2.44	  h(s(x)) -> x
4.79/2.44	
4.79/2.44	 Matrix Interpretation Processor: dim=1
4.79/2.44	  
4.79/2.44	  interpretation:
4.79/2.44	   [?2](x0, x1, x2) = 2x0 + 2x1 + x2 + 5,
4.79/2.44	   
4.79/2.44	   [h](x0) = x0 + 1,
4.79/2.44	   
4.79/2.44	   [s](x0) = x0,
4.79/2.44	   
4.79/2.44	   [a] = 6,
4.79/2.44	   
4.79/2.44	   [?1](x0, x1, x2) = 2x0 + 2x1 + 4x2 + 2,
4.79/2.44	   
4.79/2.44	   [c](x0) = x0,
4.79/2.44	   
4.79/2.44	   [g](x0) = 2x0,
4.79/2.44	   
4.79/2.44	   [f](x0, x1) = 6x0 + 6x1 + 7
4.79/2.44	  orientation:
4.79/2.44	   f(x,y) = 6x + 6y + 7 >= 6x + 4y + 2 = ?1(c(g(x)),x,y)
4.79/2.44	   
4.79/2.44	   ?1(c(a()),x,y) = 2x + 4y + 14 >= 2x = g(s(x))
4.79/2.44	   
4.79/2.44	   f(x,y) = 6x + 6y + 7 >= 4x + y + 7 = ?2(c(h(x)),x,y)
4.79/2.44	   
4.79/2.44	   ?2(c(a()),x,y) = 2x + y + 17 >= x + 1 = h(s(x))
4.79/2.44	   
4.79/2.44	   g(s(x)) = 2x >= x = x
4.79/2.44	   
4.79/2.44	   h(s(x)) = x + 1 >= x = x
4.79/2.45	  problem:
4.79/2.45	   f(x,y) -> ?2(c(h(x)),x,y)
4.79/2.45	   g(s(x)) -> x
4.79/2.45	  Matrix Interpretation Processor: dim=1
4.79/2.45	   
4.79/2.45	   interpretation:
4.79/2.45	    [?2](x0, x1, x2) = x0 + x1 + 2x2,
4.79/2.45	    
4.79/2.45	    [h](x0) = x0,
4.79/2.45	    
4.79/2.45	    [s](x0) = 6x0,
4.79/2.45	    
4.79/2.45	    [c](x0) = 6x0 + 4,
4.79/2.45	    
4.79/2.45	    [g](x0) = 3x0,
4.79/2.45	    
4.79/2.45	    [f](x0, x1) = 7x0 + 4x1 + 5
4.79/2.45	   orientation:
4.79/2.45	    f(x,y) = 7x + 4y + 5 >= 7x + 2y + 4 = ?2(c(h(x)),x,y)
4.79/2.45	    
4.79/2.45	    g(s(x)) = 18x >= x = x
4.79/2.45	   problem:
4.79/2.45	    g(s(x)) -> x
4.79/2.45	   Matrix Interpretation Processor: dim=3
4.79/2.45	    
4.79/2.45	    interpretation:
4.79/2.45	               [1 0 0]  
4.79/2.45	     [s](x0) = [0 0 1]x0
4.79/2.45	               [0 1 0]  ,
4.79/2.45	     
4.79/2.45	               [1 0 0]     [1]
4.79/2.45	     [g](x0) = [0 0 1]x0 + [0]
4.79/2.45	               [0 1 0]     [0]
4.79/2.45	    orientation:
4.79/2.45	                   [1]         
4.79/2.45	     g(s(x)) = x + [0] >= x = x
4.79/2.45	                   [0]         
4.79/2.45	    problem:
4.79/2.45	     
4.79/2.45	    Qed
4.79/2.45	All 2 critical pairs are joinable.
4.79/2.45	Overlap: (rule1: f(z, x') -> h(s(z)) <= c(h(z)) = c(a), rule2: f(y', z') -> g(s(y')) <= c(g(y')) = c(a), pos: ε, mgu: {(y',z), (z',x')})
4.79/2.45	CP: g(s(z)) = h(s(z)) <= c(h(z)) = c(a), c(g(z)) = c(a)
4.79/2.45	This critical pair is context-joinable.
4.79/2.45	Overlap: (rule1: f(z, x') -> g(s(z)) <= c(g(z)) = c(a), rule2: f(y', z') -> h(s(y')) <= c(h(y')) = c(a), pos: ε, mgu: {(y',z), (z',x')})
4.79/2.45	CP: h(s(z)) = g(s(z)) <= c(g(z)) = c(a), c(h(z)) = c(a)
4.79/2.45	This critical pair is context-joinable.
4.79/2.45	
4.91/2.49	EOF