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