4.47/2.05	YES
4.47/2.05	
4.47/2.05	Proof:
4.47/2.05	This system is confluent.
4.47/2.05	By \cite{ALS94}, Theorem 4.1.
4.47/2.05	This system is of type 3 or smaller.
4.47/2.05	This system is strongly deterministic.
4.47/2.05	This system is quasi-decreasing.
4.47/2.05	By \cite{O02}, p. 214, Proposition 7.2.50.
4.47/2.05	This system is of type 3 or smaller.
4.47/2.05	This system is deterministic.
4.47/2.05	System R transformed to U(R).
4.47/2.05	This system is terminating.
4.47/2.05	Call external tool:
4.47/2.05	./ttt2.sh
4.47/2.05	Input:
4.47/2.05	(VAR x)
4.47/2.05	(RULES
4.47/2.05	  pos(s(0)) -> true
4.47/2.05	  pos(0) -> false
4.47/2.05	  ?1(true, x) -> true
4.47/2.05	  pos(s(x)) -> ?1(pos(x), x)
4.47/2.05	  ?2(false, x) -> false
4.47/2.05	  pos(p(x)) -> ?2(pos(x), x)
4.47/2.05	)
4.47/2.05	
4.47/2.05	 Matrix Interpretation Processor: dim=1
4.47/2.05	  
4.47/2.05	  interpretation:
4.47/2.06	   [p](x0) = 2x0 + 3,
4.47/2.06	   
4.47/2.06	   [?2](x0, x1) = x0 + 2x1,
4.47/2.06	   
4.47/2.06	   [?1](x0, x1) = 4x0 + 4x1 + 2,
4.47/2.06	   
4.47/2.06	   [false] = 1,
4.47/2.06	   
4.47/2.06	   [true] = 2,
4.47/2.06	   
4.47/2.06	   [pos](x0) = 4x0 + 4,
4.47/2.06	   
4.47/2.06	   [s](x0) = 6x0 + 4,
4.47/2.06	   
4.47/2.06	   [0] = 0
4.47/2.06	  orientation:
4.47/2.06	   pos(s(0())) = 20 >= 2 = true()
4.47/2.06	   
4.47/2.06	   pos(0()) = 4 >= 1 = false()
4.47/2.06	   
4.47/2.06	   ?1(true(),x) = 4x + 10 >= 2 = true()
4.47/2.06	   
4.47/2.06	   pos(s(x)) = 24x + 20 >= 20x + 18 = ?1(pos(x),x)
4.47/2.06	   
4.47/2.06	   ?2(false(),x) = 2x + 1 >= 1 = false()
4.47/2.06	   
4.47/2.06	   pos(p(x)) = 8x + 16 >= 6x + 4 = ?2(pos(x),x)
4.47/2.06	  problem:
4.47/2.06	   ?2(false(),x) -> false()
4.47/2.06	  Matrix Interpretation Processor: dim=3
4.47/2.06	   
4.47/2.06	   interpretation:
4.47/2.06	                   [1 1 0]     [1 0 0]     [0]
4.47/2.06	    [?2](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
4.47/2.06	                   [0 0 0]     [0 0 0]     [0],
4.47/2.06	    
4.47/2.06	              [0]
4.47/2.06	    [false] = [1]
4.47/2.06	              [0]
4.47/2.06	   orientation:
4.47/2.06	                    [1 0 0]    [1]    [0]          
4.47/2.06	    ?2(false(),x) = [0 0 0]x + [1] >= [1] = false()
4.47/2.06	                    [0 0 0]    [0]    [0]          
4.47/2.06	   problem:
4.47/2.06	    
4.47/2.06	   Qed
4.47/2.06	All 2 critical pairs are joinable.
4.47/2.06	Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: pos(s(0)) -> true, pos: ε, mgu: {(y,0)})
4.47/2.06	CP: true = true <= pos(0) = true
4.47/2.06	This critical pair is context-joinable.
4.47/2.06	Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)})
4.47/2.06	CP: true = true <= pos(0) = true
4.47/2.06	This critical pair is context-joinable.
4.47/2.06	
4.75/2.08	EOF