7.02/2.59	MAYBE
7.02/2.59	
7.02/2.59	Proof:
7.02/2.59	ConCon could not decide confluence of the system.
7.02/2.59	\cite{ALS94}, Theorem 4.1 does not apply.
7.02/2.59	This system is of type 3 or smaller.
7.02/2.59	This system is strongly deterministic.
7.02/2.59	This system is quasi-decreasing.
7.02/2.59	By \cite{O02}, p. 214, Proposition 7.2.50.
7.02/2.59	This system is of type 3 or smaller.
7.02/2.60	This system is deterministic.
7.02/2.60	System R transformed to U(R).
7.02/2.60	This system is terminating.
7.02/2.60	Call external tool:
7.02/2.60	./ttt2.sh
7.02/2.60	Input:
7.02/2.60	(VAR x y)
7.02/2.60	(RULES
7.02/2.60	  ?1(d, x, y) -> g(x)
7.02/2.60	  f(x, y) -> ?1(a, x, y)
7.02/2.60	  ?2(d, x, y) -> h(x)
7.02/2.60	  f(x, y) -> ?2(b, x, y)
7.02/2.60	  g(s(x)) -> x
7.02/2.60	  h(s(x)) -> x
7.02/2.60	  a -> d
7.02/2.60	  b -> d
7.02/2.60	)
7.02/2.60	
7.02/2.60	 Matrix Interpretation Processor: dim=1
7.02/2.60	  
7.02/2.60	  interpretation:
7.02/2.60	   [s](x0) = 4x0 + 4,
7.02/2.60	   
7.02/2.60	   [b] = 0,
7.02/2.60	   
7.02/2.60	   [h](x0) = 2x0,
7.02/2.60	   
7.02/2.60	   [?2](x0, x1, x2) = x0 + 2x1 + 4x2 + 4,
7.02/2.60	   
7.02/2.60	   [a] = 0,
7.02/2.60	   
7.02/2.60	   [f](x0, x1) = 4x0 + 5x1 + 4,
7.02/2.60	   
7.02/2.60	   [g](x0) = 4x0,
7.02/2.60	   
7.02/2.60	   [?1](x0, x1, x2) = 2x0 + 4x1 + 2x2 + 4,
7.02/2.60	   
7.02/2.60	   [d] = 0
7.02/2.60	  orientation:
7.02/2.60	   ?1(d(),x,y) = 4x + 2y + 4 >= 4x = g(x)
7.02/2.60	   
7.02/2.60	   f(x,y) = 4x + 5y + 4 >= 4x + 2y + 4 = ?1(a(),x,y)
7.02/2.60	   
7.02/2.60	   ?2(d(),x,y) = 2x + 4y + 4 >= 2x = h(x)
7.02/2.60	   
7.02/2.60	   f(x,y) = 4x + 5y + 4 >= 2x + 4y + 4 = ?2(b(),x,y)
7.02/2.60	   
7.02/2.60	   g(s(x)) = 16x + 16 >= x = x
7.02/2.60	   
7.02/2.60	   h(s(x)) = 8x + 8 >= x = x
7.02/2.60	   
7.02/2.60	   a() = 0 >= 0 = d()
7.02/2.60	   
7.02/2.60	   b() = 0 >= 0 = d()
7.02/2.60	  problem:
7.02/2.60	   f(x,y) -> ?1(a(),x,y)
7.02/2.60	   f(x,y) -> ?2(b(),x,y)
7.02/2.60	   a() -> d()
7.02/2.60	   b() -> d()
7.02/2.60	  Matrix Interpretation Processor: dim=3
7.02/2.60	   
7.02/2.60	   interpretation:
7.02/2.60	          [0]
7.02/2.60	    [b] = [0]
7.02/2.60	          [0],
7.02/2.60	    
7.02/2.60	                       [1 0 0]     [1 0 0]     [1 0 0]  
7.02/2.60	    [?2](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
7.02/2.60	                       [0 0 0]     [0 0 0]     [0 0 0]  ,
7.02/2.60	    
7.02/2.60	          [0]
7.02/2.60	    [a] = [1]
7.02/2.60	          [1],
7.02/2.60	    
7.02/2.60	                  [1 0 0]     [1 0 0]     [1]
7.02/2.60	    [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
7.02/2.60	                  [0 0 0]     [0 0 0]     [1],
7.02/2.60	    
7.02/2.60	                            [1 0 0]     [1 0 0]  
7.02/2.60	    [?1](x0, x1, x2) = x0 + [0 0 0]x1 + [0 0 0]x2
7.02/2.60	                            [0 0 0]     [0 0 0]  ,
7.02/2.60	    
7.02/2.60	          [0]
7.02/2.60	    [d] = [0]
7.02/2.60	          [0]
7.02/2.60	   orientation:
7.02/2.60	             [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [0]              
7.02/2.60	    f(x,y) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [1] = ?1(a(),x,y)
7.02/2.60	             [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [1]              
7.02/2.61	    
7.02/2.61	             [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]               
7.02/2.61	    f(x,y) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y = ?2(b(),x,y)
7.02/2.61	             [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]               
7.02/2.61	    
7.02/2.61	          [0]    [0]      
7.02/2.61	    a() = [1] >= [0] = d()
7.02/2.61	          [1]    [0]      
7.02/2.61	    
7.02/2.61	          [0]    [0]      
7.02/2.61	    b() = [0] >= [0] = d()
7.02/2.61	          [0]    [0]      
7.02/2.61	   problem:
7.02/2.61	    a() -> d()
7.02/2.61	    b() -> d()
7.02/2.61	   Matrix Interpretation Processor: dim=3
7.02/2.61	    
7.02/2.61	    interpretation:
7.02/2.61	           [1]
7.02/2.61	     [b] = [0]
7.02/2.61	           [0],
7.02/2.61	     
7.02/2.61	           [0]
7.02/2.61	     [a] = [0]
7.02/2.61	           [0],
7.02/2.61	     
7.02/2.61	           [0]
7.02/2.61	     [d] = [0]
7.02/2.61	           [0]
7.02/2.61	    orientation:
7.02/2.61	           [0]    [0]      
7.02/2.61	     a() = [0] >= [0] = d()
7.02/2.61	           [0]    [0]      
7.02/2.61	     
7.02/2.61	           [1]    [0]      
7.02/2.61	     b() = [0] >= [0] = d()
7.02/2.61	           [0]    [0]      
7.02/2.61	    problem:
7.02/2.61	     a() -> d()
7.02/2.61	    Matrix Interpretation Processor: dim=3
7.02/2.61	     
7.02/2.61	     interpretation:
7.02/2.61	            [1]
7.02/2.61	      [a] = [0]
7.02/2.61	            [1],
7.02/2.61	      
7.02/2.61	            [0]
7.02/2.61	      [d] = [0]
7.02/2.61	            [0]
7.02/2.61	     orientation:
7.02/2.61	            [1]    [0]      
7.02/2.61	      a() = [0] >= [0] = d()
7.02/2.61	            [1]    [0]      
7.02/2.61	     problem:
7.02/2.61	      
7.02/2.61	     Qed
7.02/2.61	This critical pair is conditional.
7.02/2.61	This critical pair has some non-trivial conditions.
7.02/2.61	ConCon could not decide whether all 2 critical pairs are joinable or not.
7.02/2.61	Overlap: (rule1: f(z, x') -> h(z) <= b = d, rule2: f(y', z') -> g(y') <= a = d, pos: ε, mgu: {(z,y'), (x',z')})
7.02/2.61	CP: g(y') = h(y') <= b = d, a = d
7.02/2.61	ConCon could not decide infeasibility of this critical pair.
7.02/2.61	
7.02/2.63	EOF