7.47/2.76	MAYBE
7.47/2.76	
7.47/2.76	Proof:
7.47/2.76	ConCon could not decide confluence of the system.
7.47/2.76	\cite{ALS94}, Theorem 4.1 does not apply.
7.47/2.76	This system is of type 3 or smaller.
7.47/2.76	This system is strongly deterministic.
7.47/2.76	This system is quasi-decreasing.
7.47/2.76	By \cite{O02}, p. 214, Proposition 7.2.50.
7.47/2.76	This system is of type 3 or smaller.
7.47/2.76	This system is deterministic.
7.47/2.76	System R transformed to optimized U(R).
7.47/2.76	This system is terminating.
7.47/2.76	Call external tool:
7.47/2.76	./ttt2.sh
7.47/2.76	Input:
7.47/2.76	(VAR x)
7.47/2.76	(RULES
7.47/2.76	  pos(s(x)) -> ?1(pos(x), x)
7.47/2.76	  ?1(true, x) -> true
7.47/2.76	  pos(0) -> false
7.47/2.76	  p(s(x)) -> x
7.47/2.76	  s(p(x)) -> x
7.47/2.76	  pos(s(0)) -> true
7.47/2.76	  pos(p(x)) -> ?2(pos(x), x)
7.47/2.76	  ?2(false, x) -> false
7.47/2.76	)
7.47/2.76	
7.47/2.76	 Matrix Interpretation Processor: dim=1
7.47/2.76	  
7.47/2.76	  interpretation:
7.47/2.76	   [?2](x0, x1) = x0 + 2x1 + 4,
7.47/2.76	   
7.47/2.76	   [p](x0) = 3x0 + 4,
7.47/2.76	   
7.47/2.76	   [false] = 0,
7.47/2.76	   
7.47/2.76	   [0] = 2,
7.47/2.76	   
7.47/2.76	   [true] = 0,
7.47/2.76	   
7.47/2.76	   [?1](x0, x1) = x0 + x1,
7.47/2.76	   
7.47/2.76	   [pos](x0) = x0 + 7,
7.47/2.76	   
7.47/2.76	   [s](x0) = 2x0 + 1
7.47/2.76	  orientation:
7.47/2.76	   pos(s(x)) = 2x + 8 >= 2x + 7 = ?1(pos(x),x)
7.47/2.76	   
7.47/2.76	   ?1(true(),x) = x >= 0 = true()
7.47/2.76	   
7.47/2.76	   pos(0()) = 9 >= 0 = false()
7.47/2.76	   
7.47/2.76	   p(s(x)) = 6x + 7 >= x = x
7.47/2.76	   
7.47/2.76	   s(p(x)) = 6x + 9 >= x = x
7.47/2.76	   
7.47/2.76	   pos(s(0())) = 12 >= 0 = true()
7.47/2.76	   
7.47/2.76	   pos(p(x)) = 3x + 11 >= 3x + 11 = ?2(pos(x),x)
7.47/2.76	   
7.47/2.76	   ?2(false(),x) = 2x + 4 >= 0 = false()
7.47/2.76	  problem:
7.47/2.76	   ?1(true(),x) -> true()
7.47/2.76	   pos(p(x)) -> ?2(pos(x),x)
7.47/2.76	  Matrix Interpretation Processor: dim=1
7.47/2.76	   
7.47/2.76	   interpretation:
7.47/2.76	    [?2](x0, x1) = 2x0 + x1 + 2,
7.47/2.76	    
7.47/2.76	    [p](x0) = 3x0 + 5,
7.47/2.76	    
7.47/2.76	    [true] = 0,
7.47/2.76	    
7.47/2.76	    [?1](x0, x1) = x0 + 4x1 + 4,
7.47/2.76	    
7.47/2.76	    [pos](x0) = x0 + 3
7.47/2.76	   orientation:
7.47/2.76	    ?1(true(),x) = 4x + 4 >= 0 = true()
7.47/2.76	    
7.47/2.76	    pos(p(x)) = 3x + 8 >= 3x + 8 = ?2(pos(x),x)
7.47/2.76	   problem:
7.47/2.76	    pos(p(x)) -> ?2(pos(x),x)
7.47/2.76	   Matrix Interpretation Processor: dim=3
7.47/2.76	    
7.47/2.76	    interpretation:
7.47/2.76	                    [1 1 0]     [1 1 0]     [0]
7.47/2.76	     [?2](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
7.47/2.76	                    [0 0 0]     [0 0 0]     [0],
7.47/2.76	     
7.47/2.76	               [1 1 0]     [1]
7.47/2.76	     [p](x0) = [1 1 0]x0 + [1]
7.47/2.76	               [0 0 0]     [0],
7.47/2.76	     
7.47/2.76	                 [1 1 0]     [1]
7.47/2.76	     [pos](x0) = [0 0 0]x0 + [1]
7.47/2.76	                 [0 0 0]     [0]
7.47/2.76	    orientation:
7.47/2.76	                 [2 2 0]    [3]    [2 2 0]    [2]               
7.47/2.76	     pos(p(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = ?2(pos(x),x)
7.47/2.76	                 [0 0 0]    [0]    [0 0 0]    [0]               
7.47/2.76	    problem:
7.47/2.76	     
7.47/2.76	    Qed
7.47/2.76	Overlap: (rule1: s(p(y)) -> y, rule2: p(s(z)) -> z, pos: 1, mgu: {(y,s(z))})
7.47/2.76	CP: s(z) = s(z)
7.47/2.76	This critical pair is context-joinable.
7.47/2.76	Overlap: (rule1: p(s(y)) -> y, rule2: s(p(z)) -> z, pos: 1, mgu: {(y,p(z))})
7.47/2.76	CP: p(z) = p(z)
7.47/2.76	This critical pair is context-joinable.
7.47/2.76	Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)})
7.47/2.76	CP: true = true <= pos(0) = true
7.47/2.76	This critical pair is context-joinable.
7.47/2.77	This critical pair is conditional.
7.47/2.77	This critical pair has some non-trivial conditions.
7.47/2.77	ConCon could not decide whether all 6 critical pairs are joinable or not.
7.47/2.77	Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: s(p(z)) -> z, pos: 1, mgu: {(y,p(z))})
7.47/2.77	CP: pos(z) = true <= pos(p(z)) = true
7.47/2.77	ConCon could not decide infeasibility of this critical pair.
7.47/2.77	
7.47/2.80	EOF