4.55/2.03	YES
4.55/2.03	
4.55/2.03	Proof:
4.55/2.03	This system is confluent.
4.55/2.03	By \cite{ALS94}, Theorem 4.1.
4.55/2.03	This system is of type 3 or smaller.
4.55/2.03	This system is strongly deterministic.
4.55/2.03	This system is quasi-decreasing.
4.55/2.03	By \cite{A14}, Theorem 11.5.9.
4.55/2.03	This system is of type 3 or smaller.
4.55/2.03	This system is deterministic.
4.55/2.03	System R transformed to V(R) + Emb.
4.55/2.03	This system is terminating.
4.55/2.03	Call external tool:
4.55/2.03	./ttt2.sh
4.55/2.03	Input:
4.55/2.03	(VAR x)
4.55/2.03	(RULES
4.55/2.03	  pos(s(0)) -> true
4.55/2.03	  pos(0) -> false
4.55/2.03	  pos(s(x)) -> true
4.55/2.03	  pos(s(x)) -> pos(x)
4.55/2.03	  pos(p(x)) -> false
4.55/2.03	  pos(p(x)) -> pos(x)
4.55/2.03	  pos(x) -> x
4.55/2.03	  p(x) -> x
4.55/2.03	  s(x) -> x
4.55/2.03	)
4.55/2.03	
4.55/2.03	 Matrix Interpretation Processor: dim=3
4.55/2.03	  
4.55/2.03	  interpretation:
4.55/2.03	               
4.55/2.03	   [p](x0) = x0
4.55/2.03	               ,
4.55/2.03	   
4.55/2.03	             [0]
4.55/2.03	   [false] = [0]
4.55/2.03	             [0],
4.55/2.03	   
4.55/2.03	            [0]
4.55/2.03	   [true] = [0]
4.55/2.03	            [0],
4.55/2.03	   
4.55/2.03	                    [1]
4.55/2.03	   [pos](x0) = x0 + [0]
4.55/2.03	                    [0],
4.55/2.03	   
4.55/2.03	               
4.55/2.03	   [s](x0) = x0
4.55/2.03	               ,
4.55/2.03	   
4.55/2.03	         [0]
4.55/2.03	   [0] = [0]
4.55/2.03	         [0]
4.55/2.03	  orientation:
4.55/2.03	                 [1]    [0]         
4.55/2.03	   pos(s(0())) = [0] >= [0] = true()
4.55/2.03	                 [0]    [0]         
4.55/2.03	   
4.55/2.04	              [1]    [0]          
4.55/2.04	   pos(0()) = [0] >= [0] = false()
4.55/2.04	              [0]    [0]          
4.55/2.04	   
4.55/2.04	                   [1]    [0]         
4.55/2.04	   pos(s(x)) = x + [0] >= [0] = true()
4.55/2.04	                   [0]    [0]         
4.55/2.04	   
4.55/2.04	                   [1]        [1]         
4.55/2.04	   pos(s(x)) = x + [0] >= x + [0] = pos(x)
4.55/2.04	                   [0]        [0]         
4.55/2.04	   
4.55/2.04	                   [1]    [0]          
4.55/2.04	   pos(p(x)) = x + [0] >= [0] = false()
4.55/2.04	                   [0]    [0]          
4.55/2.04	   
4.55/2.04	                   [1]        [1]         
4.55/2.04	   pos(p(x)) = x + [0] >= x + [0] = pos(x)
4.55/2.04	                   [0]        [0]         
4.55/2.04	   
4.55/2.04	                [1]         
4.55/2.04	   pos(x) = x + [0] >= x = x
4.55/2.04	                [0]         
4.55/2.04	   
4.55/2.04	                    
4.55/2.04	   p(x) = x >= x = x
4.55/2.04	                    
4.55/2.04	   
4.55/2.04	                    
4.55/2.04	   s(x) = x >= x = x
4.55/2.04	                    
4.55/2.04	  problem:
4.55/2.04	   pos(s(x)) -> pos(x)
4.55/2.04	   pos(p(x)) -> pos(x)
4.55/2.04	   p(x) -> x
4.55/2.04	   s(x) -> x
4.55/2.04	  Matrix Interpretation Processor: dim=3
4.55/2.04	   
4.55/2.04	   interpretation:
4.55/2.04	                   [1]
4.55/2.04	    [p](x0) = x0 + [0]
4.55/2.04	                   [0],
4.55/2.04	    
4.55/2.04	                [1 0 0]     [0]
4.55/2.04	    [pos](x0) = [0 0 0]x0 + [0]
4.55/2.04	                [0 0 0]     [1],
4.55/2.04	    
4.55/2.04	                   [1]
4.55/2.04	    [s](x0) = x0 + [0]
4.55/2.04	                   [0]
4.55/2.04	   orientation:
4.55/2.04	                [1 0 0]    [1]    [1 0 0]    [0]         
4.55/2.04	    pos(s(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = pos(x)
4.55/2.04	                [0 0 0]    [1]    [0 0 0]    [1]         
4.55/2.04	    
4.55/2.04	                [1 0 0]    [1]    [1 0 0]    [0]         
4.55/2.04	    pos(p(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = pos(x)
4.55/2.04	                [0 0 0]    [1]    [0 0 0]    [1]         
4.55/2.04	    
4.55/2.04	               [1]         
4.55/2.04	    p(x) = x + [0] >= x = x
4.55/2.04	               [0]         
4.55/2.04	    
4.55/2.04	               [1]         
4.55/2.04	    s(x) = x + [0] >= x = x
4.55/2.04	               [0]         
4.55/2.04	   problem:
4.55/2.04	    
4.55/2.04	   Qed
4.55/2.04	All 2 critical pairs are joinable.
4.55/2.04	Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: pos(s(0)) -> true, pos: ε, mgu: {(y,0)})
4.55/2.04	CP: true = true <= pos(0) = true
4.55/2.04	This critical pair is context-joinable.
4.55/2.04	Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)})
4.55/2.04	CP: true = true <= pos(0) = true
4.55/2.04	This critical pair is context-joinable.
4.55/2.04	
4.79/2.09	EOF