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