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