YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: size(empty) -> 0 size(push(x, y)) -> s(size(x)) m -> s(s(s(s(0)))) pop(empty) -> empty ?1(true, x, y) -> x pop(push(x, y)) -> ?1(le(size(x), m), x, y) top(empty) -> eentry ?2(true, x, y) -> y top(push(x, y)) -> ?2(le(size(x), m), x, y) le(x, 0) -> false le(0, s(x)) -> true le(s(x), s(y)) -> le(x, y) DP Processor: DPs: size#(push(x,y)) -> size#(x) pop#(push(x,y)) -> m#() pop#(push(x,y)) -> size#(x) pop#(push(x,y)) -> le#(size(x),m()) pop#(push(x,y)) -> ?1#(le(size(x),m()),x,y) top#(push(x,y)) -> m#() top#(push(x,y)) -> size#(x) top#(push(x,y)) -> le#(size(x),m()) top#(push(x,y)) -> ?2#(le(size(x),m()),x,y) le#(s(x),s(y)) -> le#(x,y) TRS: size(empty()) -> 0() size(push(x,y)) -> s(size(x)) m() -> s(s(s(s(0())))) pop(empty()) -> empty() ?1(true(),x,y) -> x pop(push(x,y)) -> ?1(le(size(x),m()),x,y) top(empty()) -> eentry() ?2(true(),x,y) -> y top(push(x,y)) -> ?2(le(size(x),m()),x,y) le(x,0()) -> false() le(0(),s(x)) -> true() le(s(x),s(y)) -> le(x,y) TDG Processor: DPs: size#(push(x,y)) -> size#(x) pop#(push(x,y)) -> m#() pop#(push(x,y)) -> size#(x) pop#(push(x,y)) -> le#(size(x),m()) pop#(push(x,y)) -> ?1#(le(size(x),m()),x,y) top#(push(x,y)) -> m#() top#(push(x,y)) -> size#(x) top#(push(x,y)) -> le#(size(x),m()) top#(push(x,y)) -> ?2#(le(size(x),m()),x,y) le#(s(x),s(y)) -> le#(x,y) TRS: size(empty()) -> 0() size(push(x,y)) -> s(size(x)) m() -> s(s(s(s(0())))) pop(empty()) -> empty() ?1(true(),x,y) -> x pop(push(x,y)) -> ?1(le(size(x),m()),x,y) top(empty()) -> eentry() ?2(true(),x,y) -> y top(push(x,y)) -> ?2(le(size(x),m()),x,y) le(x,0()) -> false() le(0(),s(x)) -> true() le(s(x),s(y)) -> le(x,y) graph: top#(push(x,y)) -> le#(size(x),m()) -> le#(s(x),s(y)) -> le#(x,y) top#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> size#(x) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) pop#(push(x,y)) -> le#(size(x),m()) -> le#(s(x),s(y)) -> le#(x,y) pop#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> size#(x) size#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> size#(x) SCC Processor: #sccs: 2 #rules: 2 #arcs: 6/100 DPs: size#(push(x,y)) -> size#(x) TRS: size(empty()) -> 0() size(push(x,y)) -> s(size(x)) m() -> s(s(s(s(0())))) pop(empty()) -> empty() ?1(true(),x,y) -> x pop(push(x,y)) -> ?1(le(size(x),m()),x,y) top(empty()) -> eentry() ?2(true(),x,y) -> y top(push(x,y)) -> ?2(le(size(x),m()),x,y) le(x,0()) -> false() le(0(),s(x)) -> true() le(s(x),s(y)) -> le(x,y) Subterm Criterion Processor: simple projection: pi(size#) = 0 problem: DPs: TRS: size(empty()) -> 0() size(push(x,y)) -> s(size(x)) m() -> s(s(s(s(0())))) pop(empty()) -> empty() ?1(true(),x,y) -> x pop(push(x,y)) -> ?1(le(size(x),m()),x,y) top(empty()) -> eentry() ?2(true(),x,y) -> y top(push(x,y)) -> ?2(le(size(x),m()),x,y) le(x,0()) -> false() le(0(),s(x)) -> true() le(s(x),s(y)) -> le(x,y) Qed DPs: le#(s(x),s(y)) -> le#(x,y) TRS: size(empty()) -> 0() size(push(x,y)) -> s(size(x)) m() -> s(s(s(s(0())))) pop(empty()) -> empty() ?1(true(),x,y) -> x pop(push(x,y)) -> ?1(le(size(x),m()),x,y) top(empty()) -> eentry() ?2(true(),x,y) -> y top(push(x,y)) -> ?2(le(size(x),m()),x,y) le(x,0()) -> false() le(0(),s(x)) -> true() le(s(x),s(y)) -> le(x,y) Subterm Criterion Processor: simple projection: pi(le#) = 0 problem: DPs: TRS: size(empty()) -> 0() size(push(x,y)) -> s(size(x)) m() -> s(s(s(s(0())))) pop(empty()) -> empty() ?1(true(),x,y) -> x pop(push(x,y)) -> ?1(le(size(x),m()),x,y) top(empty()) -> eentry() ?2(true(),x,y) -> y top(push(x,y)) -> ?2(le(size(x),m()),x,y) le(x,0()) -> false() le(0(),s(x)) -> true() le(s(x),s(y)) -> le(x,y) Qed