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