7.71/2.45	YES
7.71/2.45	
7.71/2.45	Problem:
7.71/2.45	pos(s(0())) -> true()
7.71/2.45	pos(0()) -> false()
7.71/2.45	pos(s(x)) -> true() <= pos(x) = true()
7.71/2.45	pos(p(x)) -> false() <= pos(x) = false()
7.71/2.45	
7.71/2.45	Proof:
7.71/2.45	This system is confluent.
7.71/2.45	By \cite{ALS94}, Theorem 4.1.
7.71/2.45	This system is of type 3 or smaller.
7.71/2.45	This system is strongly deterministic.
7.71/2.45	All 2 critical pairs are joinable.
7.71/2.45	CP: true() = true() <= pos(0()) = true():
7.71/2.45	This critical pair is context-joinable.
7.71/2.45	CP: true() = true() <= pos(0()) = true():
7.71/2.45	This critical pair is context-joinable.
7.71/2.45	This system is quasi-decreasing.
7.71/2.45	By \cite{O02}, p. 214, Proposition 7.2.50.
7.71/2.45	This system is of type 3 or smaller.
7.71/2.45	This system is deterministic.
7.71/2.45	System R transformed to U(R).
7.71/2.45	This system is terminating.
7.71/2.45	Call external tool:
7.71/2.45	./ttt2.sh
7.71/2.45	Input:
7.71/2.45	  pos(s(0())) -> true()
7.71/2.45	  pos(0()) -> false()
7.71/2.45	  ?2(true(), x) -> true()
7.71/2.45	  pos(s(x)) -> ?2(pos(x), x)
7.71/2.45	  ?1(false(), x) -> false()
7.71/2.45	  pos(p(x)) -> ?1(pos(x), x)
7.71/2.45	
7.71/2.45	 Matrix Interpretation Processor: dim=1
7.71/2.45	  
7.71/2.45	  interpretation:
7.71/2.45	   [p](x0) = 3x0,
7.71/2.45	   
7.71/2.45	   [?1](x0, x1) = x0 + 2x1,
7.71/2.45	   
7.71/2.45	   [?2](x0, x1) = 2x0 + 4x1,
7.71/2.45	   
7.71/2.45	   [false] = 5,
7.71/2.45	   
7.71/2.45	   [true] = 0,
7.71/2.45	   
7.71/2.45	   [pos](x0) = x0 + 3,
7.71/2.45	   
7.71/2.45	   [s](x0) = 7x0 + 4,
7.71/2.45	   
7.71/2.45	   [0] = 2
7.71/2.45	  orientation:
7.71/2.45	   pos(s(0())) = 21 >= 0 = true()
7.71/2.45	   
7.71/2.45	   pos(0()) = 5 >= 5 = false()
7.71/2.45	   
7.71/2.45	   ?2(true(),x) = 4x >= 0 = true()
7.71/2.45	   
7.71/2.45	   pos(s(x)) = 7x + 7 >= 6x + 6 = ?2(pos(x),x)
7.71/2.45	   
7.71/2.46	   ?1(false(),x) = 2x + 5 >= 5 = false()
7.71/2.46	   
7.71/2.47	   pos(p(x)) = 3x + 3 >= 3x + 3 = ?1(pos(x),x)
7.71/2.47	  problem:
7.71/2.47	   pos(0()) -> false()
7.71/2.47	   ?2(true(),x) -> true()
7.71/2.47	   ?1(false(),x) -> false()
7.71/2.47	   pos(p(x)) -> ?1(pos(x),x)
7.71/2.47	  Matrix Interpretation Processor: dim=1
7.71/2.47	   
7.71/2.47	   interpretation:
7.71/2.47	    [p](x0) = 4x0,
7.71/2.47	    
7.71/2.47	    [?1](x0, x1) = 2x0 + 4x1,
7.71/2.47	    
7.71/2.47	    [?2](x0, x1) = x0 + 2x1,
7.71/2.47	    
7.71/2.47	    [false] = 0,
7.71/2.47	    
7.71/2.47	    [true] = 0,
7.71/2.47	    
7.71/2.47	    [pos](x0) = 2x0,
7.71/2.47	    
7.71/2.47	    [0] = 4
7.71/2.47	   orientation:
7.71/2.47	    pos(0()) = 8 >= 0 = false()
7.71/2.47	    
7.71/2.47	    ?2(true(),x) = 2x >= 0 = true()
7.71/2.47	    
7.71/2.47	    ?1(false(),x) = 4x >= 0 = false()
7.71/2.47	    
7.71/2.47	    pos(p(x)) = 8x >= 8x = ?1(pos(x),x)
7.71/2.47	   problem:
7.71/2.47	    ?2(true(),x) -> true()
7.71/2.47	    ?1(false(),x) -> false()
7.71/2.47	    pos(p(x)) -> ?1(pos(x),x)
7.71/2.47	   Matrix Interpretation Processor: dim=1
7.71/2.47	    
7.71/2.47	    interpretation:
7.71/2.47	     [p](x0) = 5x0,
7.71/2.47	     
7.71/2.47	     [?1](x0, x1) = x0 + 4x1,
7.71/2.47	     
7.71/2.47	     [?2](x0, x1) = x0 + 2x1 + 1,
7.71/2.47	     
7.71/2.47	     [false] = 4,
7.71/2.47	     
7.71/2.47	     [true] = 3,
7.71/2.47	     
7.71/2.47	     [pos](x0) = x0
7.71/2.47	    orientation:
7.71/2.47	     ?2(true(),x) = 2x + 4 >= 3 = true()
7.71/2.47	     
7.71/2.47	     ?1(false(),x) = 4x + 4 >= 4 = false()
7.71/2.47	     
7.71/2.47	     pos(p(x)) = 5x >= 5x = ?1(pos(x),x)
7.71/2.47	    problem:
7.71/2.47	     ?1(false(),x) -> false()
7.71/2.47	     pos(p(x)) -> ?1(pos(x),x)
7.71/2.47	    Matrix Interpretation Processor: dim=3
7.71/2.47	     
7.71/2.47	     interpretation:
7.71/2.47	                [1 0 0]  
7.71/2.47	      [p](x0) = [0 0 0]x0
7.71/2.47	                [1 0 1]  ,
7.71/2.47	      
7.71/2.47	                     [1 0 1]     [1 0 0]     [0]
7.71/2.47	      [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
7.71/2.47	                     [0 0 1]     [0 0 0]     [0],
7.71/2.47	      
7.71/2.47	                [1]
7.71/2.47	      [false] = [1]
7.71/2.47	                [1],
7.71/2.47	      
7.71/2.47	                  [1 0 1]     [0]
7.71/2.47	      [pos](x0) = [0 0 0]x0 + [1]
7.71/2.47	                  [0 0 0]     [0]
7.71/2.47	     orientation:
7.71/2.47	                      [1 0 0]    [2]    [1]          
7.71/2.47	      ?1(false(),x) = [0 0 0]x + [1] >= [1] = false()
7.71/2.47	                      [0 0 0]    [1]    [1]          
7.71/2.47	      
7.71/2.47	                  [2 0 1]    [0]    [2 0 1]    [0]               
7.71/2.47	      pos(p(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = ?1(pos(x),x)
7.71/2.47	                  [0 0 0]    [0]    [0 0 0]    [0]               
7.71/2.47	     problem:
7.71/2.47	      pos(p(x)) -> ?1(pos(x),x)
7.71/2.47	     Matrix Interpretation Processor: dim=1
7.71/2.47	      
7.71/2.47	      interpretation:
7.71/2.47	       [p](x0) = 6x0 + 4,
7.71/2.47	       
7.71/2.47	       [?1](x0, x1) = x0 + 5x1 + 3,
7.71/2.47	       
7.71/2.47	       [pos](x0) = x0 + 1
7.71/2.47	      orientation:
7.71/2.47	       pos(p(x)) = 6x + 5 >= 6x + 4 = ?1(pos(x),x)
7.71/2.47	      problem:
7.71/2.47	       
7.71/2.47	      Qed
7.71/2.47	
8.02/2.59	EOF