6.64/2.59	YES
6.64/2.59	
6.64/2.59	Proof:
6.64/2.59	This system is confluent.
6.64/2.59	By \cite{ALS94}, Theorem 4.1.
6.64/2.59	This system is of type 3 or smaller.
6.64/2.59	This system is strongly deterministic.
6.64/2.59	This system is quasi-decreasing.
6.64/2.59	By \cite{O02}, p. 214, Proposition 7.2.50.
6.64/2.59	This system is of type 3 or smaller.
6.64/2.59	This system is deterministic.
6.64/2.59	System R transformed to optimized U(R).
6.64/2.59	This system is terminating.
6.64/2.59	Call external tool:
6.64/2.59	./ttt2.sh
6.64/2.59	Input:
6.64/2.59	(VAR x y)
6.64/2.59	(RULES
6.64/2.59	  pop(empty) -> empty
6.64/2.59	  le(0, s(x)) -> true
6.64/2.59	  top(push(x, y)) -> ?2(le(size(x), m), x, y)
6.64/2.59	  ?2(true, x, y) -> y
6.64/2.59	  le(s(x), s(y)) -> le(x, y)
6.64/2.59	  size(push(x, y)) -> s(size(x))
6.64/2.59	  size(empty) -> 0
6.64/2.59	  le(x, 0) -> false
6.64/2.59	  pop(push(x, y)) -> ?1(le(size(x), m), x, y)
6.64/2.59	  ?1(true, x, y) -> x
6.64/2.59	  m -> s(s(s(s(0))))
6.64/2.59	  top(empty) -> eentry
6.64/2.59	)
6.64/2.59	
6.64/2.59	 Matrix Interpretation Processor: dim=1
6.64/2.59	  
6.64/2.59	  interpretation:
6.64/2.59	   [eentry] = 0,
6.64/2.59	   
6.64/2.59	   [?1](x0, x1, x2) = 3x0 + x1 + x2 + 3,
6.64/2.59	   
6.64/2.59	   [false] = 0,
6.64/2.59	   
6.64/2.59	   [?2](x0, x1, x2) = x0 + x1 + 2x2 + 7,
6.64/2.59	   
6.64/2.59	   [m] = 0,
6.64/2.59	   
6.64/2.59	   [size](x0) = 2x0,
6.64/2.59	   
6.64/2.59	   [top](x0) = 4x0,
6.64/2.59	   
6.64/2.59	   [push](x0, x1) = 5x0 + 2x1 + 3,
6.64/2.59	   
6.64/2.59	   [true] = 1,
6.64/2.59	   
6.64/2.59	   [le](x0, x1) = 4x0 + 4x1 + 1,
6.64/2.59	   
6.64/2.59	   [s](x0) = 2x0,
6.64/2.59	   
6.64/2.59	   [0] = 0,
6.64/2.59	   
6.64/2.59	   [pop](x0) = 5x0 + 5,
6.64/2.59	   
6.64/2.59	   [empty] = 0
6.64/2.59	  orientation:
6.64/2.59	   pop(empty()) = 5 >= 0 = empty()
6.64/2.59	   
6.64/2.59	   le(0(),s(x)) = 8x + 1 >= 1 = true()
6.64/2.59	   
6.64/2.59	   top(push(x,y)) = 20x + 8y + 12 >= 9x + 2y + 8 = ?2(le(size(x),m()),x,y)
6.64/2.59	   
6.64/2.59	   ?2(true(),x,y) = x + 2y + 8 >= y = y
6.64/2.59	   
6.64/2.59	   le(s(x),s(y)) = 8x + 8y + 1 >= 4x + 4y + 1 = le(x,y)
6.64/2.59	   
6.64/2.59	   size(push(x,y)) = 10x + 4y + 6 >= 4x = s(size(x))
6.64/2.59	   
6.64/2.59	   size(empty()) = 0 >= 0 = 0()
6.64/2.59	   
6.64/2.59	   le(x,0()) = 4x + 1 >= 0 = false()
6.64/2.59	   
6.64/2.59	   pop(push(x,y)) = 25x + 10y + 20 >= 25x + y + 6 = ?1(le(size(x),m()),x,y)
6.64/2.59	   
6.64/2.59	   ?1(true(),x,y) = x + y + 6 >= x = x
6.64/2.59	   
6.64/2.59	   m() = 0 >= 0 = s(s(s(s(0()))))
6.64/2.59	   
6.64/2.59	   top(empty()) = 0 >= 0 = eentry()
6.72/2.60	  problem:
6.72/2.60	   le(0(),s(x)) -> true()
6.72/2.60	   le(s(x),s(y)) -> le(x,y)
6.72/2.60	   size(empty()) -> 0()
6.72/2.60	   m() -> s(s(s(s(0()))))
6.72/2.60	   top(empty()) -> eentry()
6.72/2.60	  Matrix Interpretation Processor: dim=3
6.72/2.60	   
6.72/2.60	   interpretation:
6.72/2.60	               [0]
6.72/2.60	    [eentry] = [0]
6.72/2.60	               [0],
6.72/2.60	    
6.72/2.60	          [1]
6.72/2.60	    [m] = [0]
6.72/2.60	          [0],
6.72/2.60	    
6.72/2.60	                 [1 0 0]  
6.72/2.60	    [size](x0) = [0 0 0]x0
6.72/2.60	                 [0 0 0]  ,
6.72/2.60	    
6.72/2.60	                [1 0 0]  
6.72/2.60	    [top](x0) = [0 1 0]x0
6.72/2.60	                [0 0 0]  ,
6.72/2.60	    
6.72/2.60	             [0]
6.72/2.60	    [true] = [0]
6.72/2.60	             [0],
6.72/2.60	    
6.72/2.60	                   [1 0 0]     [1 0 0]     [1]
6.72/2.60	    [le](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
6.72/2.60	                   [0 0 0]     [0 0 0]     [0],
6.72/2.60	    
6.72/2.60	              [1 1 0]  
6.72/2.60	    [s](x0) = [0 0 0]x0
6.72/2.60	              [0 0 0]  ,
6.72/2.60	    
6.72/2.60	          [0]
6.72/2.60	    [0] = [0]
6.72/2.60	          [0],
6.72/2.60	    
6.72/2.60	              [0]
6.72/2.60	    [empty] = [1]
6.72/2.60	              [0]
6.72/2.60	   orientation:
6.72/2.60	                   [1 1 0]    [1]    [0]         
6.72/2.60	    le(0(),s(x)) = [0 0 0]x + [0] >= [0] = true()
6.72/2.60	                   [0 0 0]    [0]    [0]         
6.72/2.60	    
6.72/2.60	                    [1 1 0]    [1 1 0]    [1]    [1 0 0]    [1 0 0]    [1]          
6.72/2.60	    le(s(x),s(y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = le(x,y)
6.72/2.60	                    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]          
6.72/2.60	    
6.72/2.60	                    [0]    [0]      
6.72/2.60	    size(empty()) = [0] >= [0] = 0()
6.72/2.60	                    [0]    [0]      
6.72/2.60	    
6.72/2.60	          [1]    [0]                  
6.72/2.60	    m() = [0] >= [0] = s(s(s(s(0()))))
6.72/2.60	          [0]    [0]                  
6.72/2.60	    
6.72/2.60	                   [0]    [0]           
6.72/2.60	    top(empty()) = [1] >= [0] = eentry()
6.72/2.60	                   [0]    [0]           
6.72/2.60	   problem:
6.72/2.60	    le(s(x),s(y)) -> le(x,y)
6.72/2.60	    size(empty()) -> 0()
6.72/2.60	    top(empty()) -> eentry()
6.72/2.60	   Matrix Interpretation Processor: dim=3
6.72/2.60	    
6.72/2.60	    interpretation:
6.72/2.60	                [0]
6.72/2.60	     [eentry] = [0]
6.72/2.60	                [0],
6.72/2.60	     
6.72/2.60	                  [1 0 1]  
6.72/2.60	     [size](x0) = [0 0 0]x0
6.72/2.60	                  [0 0 0]  ,
6.72/2.60	     
6.72/2.60	                 [1 0 0]     [1]
6.72/2.60	     [top](x0) = [0 0 0]x0 + [0]
6.72/2.60	                 [0 0 0]     [0],
6.72/2.61	     
6.72/2.61	                    [1 0 0]     [1 0 1]  
6.72/2.61	     [le](x0, x1) = [0 0 0]x0 + [0 0 0]x1
6.72/2.61	                    [0 0 0]     [0 0 0]  ,
6.72/2.61	     
6.72/2.61	               [1 0 0]     [0]
6.72/2.61	     [s](x0) = [0 0 0]x0 + [0]
6.72/2.61	               [0 0 1]     [1],
6.72/2.61	     
6.72/2.61	           [0]
6.72/2.61	     [0] = [0]
6.72/2.61	           [0],
6.72/2.61	     
6.72/2.61	               [0]
6.72/2.61	     [empty] = [0]
6.72/2.61	               [1]
6.72/2.61	    orientation:
6.72/2.61	                     [1 0 0]    [1 0 1]    [1]    [1 0 0]    [1 0 1]           
6.72/2.61	     le(s(x),s(y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = le(x,y)
6.72/2.61	                     [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]           
6.72/2.61	     
6.72/2.61	                     [1]    [0]      
6.72/2.61	     size(empty()) = [0] >= [0] = 0()
6.72/2.61	                     [0]    [0]      
6.72/2.61	     
6.72/2.61	                    [1]    [0]           
6.72/2.61	     top(empty()) = [0] >= [0] = eentry()
6.72/2.61	                    [0]    [0]           
6.72/2.61	    problem:
6.72/2.61	     
6.72/2.61	    Qed
6.72/2.61	All 0 critical pairs are joinable.
6.72/2.61	
7.20/2.77	EOF