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