YES Time: 0.100551 TRS: { mark nil() -> nil(), mark cons(X1, X2) -> cons(mark X1, X2), mark app(X1, X2) -> a__app(mark X1, mark X2), mark from X -> a__from mark X, mark s X -> s mark X, mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2), mark prefix X -> a__prefix mark X, a__app(X1, X2) -> app(X1, X2), a__app(nil(), YS) -> mark YS, a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)), a__from X -> cons(mark X, from s X), a__from X -> from X, a__zWadr(XS, nil()) -> nil(), a__zWadr(X1, X2) -> zWadr(X1, X2), a__zWadr(nil(), YS) -> nil(), a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)), a__prefix X -> prefix X, a__prefix L -> cons(nil(), zWadr(L, prefix L))} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), mark# prefix X -> mark# X, mark# prefix X -> a__prefix# mark X, a__app#(nil(), YS) -> mark# YS, a__app#(cons(X, XS), YS) -> mark# X, a__from# X -> mark# X, a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))} TRS: { mark nil() -> nil(), mark cons(X1, X2) -> cons(mark X1, X2), mark app(X1, X2) -> a__app(mark X1, mark X2), mark from X -> a__from mark X, mark s X -> s mark X, mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2), mark prefix X -> a__prefix mark X, a__app(X1, X2) -> app(X1, X2), a__app(nil(), YS) -> mark YS, a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)), a__from X -> cons(mark X, from s X), a__from X -> from X, a__zWadr(XS, nil()) -> nil(), a__zWadr(X1, X2) -> zWadr(X1, X2), a__zWadr(nil(), YS) -> nil(), a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)), a__prefix X -> prefix X, a__prefix L -> cons(nil(), zWadr(L, prefix L))} EDG: { (mark# from X -> mark# X, mark# prefix X -> a__prefix# mark X) (mark# from X -> mark# X, mark# prefix X -> mark# X) (mark# from X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# from X -> mark# X, mark# zWadr(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# zWadr(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# from X -> mark# X, mark# app(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# app(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# prefix X -> mark# X, mark# prefix X -> a__prefix# mark X) (mark# prefix X -> mark# X, mark# prefix X -> mark# X) (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> mark# X2) (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> mark# X1) (mark# prefix X -> mark# X, mark# s X -> mark# X) (mark# prefix X -> mark# X, mark# from X -> a__from# mark X) (mark# prefix X -> mark# X, mark# from X -> mark# X) (mark# prefix X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# prefix X -> mark# X, mark# app(X1, X2) -> mark# X2) (mark# prefix X -> mark# X, mark# app(X1, X2) -> mark# X1) (mark# prefix X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# prefix X -> a__prefix# mark X) (a__from# X -> mark# X, mark# prefix X -> mark# X) (a__from# X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# app(X1, X2) -> mark# X2, mark# prefix X -> a__prefix# mark X) (mark# app(X1, X2) -> mark# X2, mark# prefix X -> mark# X) (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X2) (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X1) (mark# app(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# app(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# app(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X2) (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X1) (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(cons(X, XS), YS) -> mark# X) (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(nil(), YS) -> mark# YS) (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> a__prefix# mark X) (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> mark# X) (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X2) (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X1) (a__app#(nil(), YS) -> mark# YS, mark# s X -> mark# X) (a__app#(nil(), YS) -> mark# YS, mark# from X -> a__from# mark X) (a__app#(nil(), YS) -> mark# YS, mark# from X -> mark# X) (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X2) (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X1) (a__app#(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> mark# X1) (mark# app(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X) (mark# app(X1, X2) -> mark# X1, mark# prefix X -> mark# X) (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2) (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1) (mark# app(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# app(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# app(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2) (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1) (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> a__prefix# mark X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> mark# X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X2) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X1) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# s X -> mark# X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> a__from# mark X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> mark# X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X2) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X1) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2) (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2) (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# zWadr(X1, X2) -> mark# X1, mark# prefix X -> mark# X) (mark# zWadr(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X) (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X) (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y) (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))) (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X2) (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X1) (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X2) (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# zWadr(X1, X2) -> mark# X2, mark# prefix X -> mark# X) (mark# zWadr(X1, X2) -> mark# X2, mark# prefix X -> a__prefix# mark X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X1) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X2) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> mark# X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> a__from# mark X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# s X -> mark# X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X1) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X2) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> mark# X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> a__prefix# mark X) (a__app#(cons(X, XS), YS) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X1) (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X2) (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> mark# X) (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> a__from# mark X) (a__app#(cons(X, XS), YS) -> mark# X, mark# s X -> mark# X) (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X1) (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X2) (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> mark# X) (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> a__prefix# mark X) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# app(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# app(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2)) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2)) (mark# s X -> mark# X, mark# prefix X -> mark# X) (mark# s X -> mark# X, mark# prefix X -> a__prefix# mark X) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(nil(), YS) -> mark# YS) (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(cons(X, XS), YS) -> mark# X) (mark# from X -> a__from# mark X, a__from# X -> mark# X) } STATUS: arrows: 0.493827 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), mark# prefix X -> mark# X, a__app#(nil(), YS) -> mark# YS, a__app#(cons(X, XS), YS) -> mark# X, a__from# X -> mark# X, a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))} SCC (17): Strict: { mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), mark# prefix X -> mark# X, a__app#(nil(), YS) -> mark# YS, a__app#(cons(X, XS), YS) -> mark# X, a__from# X -> mark# X, a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))} Weak: { mark nil() -> nil(), mark cons(X1, X2) -> cons(mark X1, X2), mark app(X1, X2) -> a__app(mark X1, mark X2), mark from X -> a__from mark X, mark s X -> s mark X, mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2), mark prefix X -> a__prefix mark X, a__app(X1, X2) -> app(X1, X2), a__app(nil(), YS) -> mark YS, a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)), a__from X -> cons(mark X, from s X), a__from X -> from X, a__zWadr(XS, nil()) -> nil(), a__zWadr(X1, X2) -> zWadr(X1, X2), a__zWadr(nil(), YS) -> nil(), a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)), a__prefix X -> prefix X, a__prefix L -> cons(nil(), zWadr(L, prefix L))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__app](x0, x1) = x0 + x1, [cons](x0, x1) = x0, [app](x0, x1) = x0 + x1, [a__zWadr](x0, x1) = x0 + x1 + 1, [zWadr](x0, x1) = x0 + x1 + 1, [mark](x0) = x0, [from](x0) = x0 + 1, [s](x0) = x0, [a__from](x0) = x0 + 1, [prefix](x0) = x0, [a__prefix](x0) = x0, [nil] = 0, [a__app#](x0, x1) = x0 + x1, [a__zWadr#](x0, x1) = x0 + x1 + 1, [mark#](x0) = x0, [a__from#](x0) = x0 Strict: a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())) 1 + 0YS + 1X + 0XS + 1Y >= 0 + 1X + 1Y a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y 1 + 0YS + 1X + 0XS + 1Y >= 0 + 1Y a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X 1 + 0YS + 1X + 0XS + 1Y >= 0 + 1X a__from# X -> mark# X 0 + 1X >= 0 + 1X a__app#(cons(X, XS), YS) -> mark# X 0 + 1YS + 1X + 0XS >= 0 + 1X a__app#(nil(), YS) -> mark# YS 0 + 1YS >= 0 + 1YS mark# prefix X -> mark# X 0 + 1X >= 0 + 1X mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark# zWadr(X1, X2) -> mark# X2 1 + 1X1 + 1X2 >= 0 + 1X2 mark# zWadr(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# from X -> a__from# mark X 1 + 1X >= 0 + 1X mark# from X -> mark# X 1 + 1X >= 0 + 1X mark# app(X1, X2) -> a__app#(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# app(X1, X2) -> mark# X2 0 + 1X1 + 1X2 >= 0 + 1X2 mark# app(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 Weak: a__prefix L -> cons(nil(), zWadr(L, prefix L)) 0 + 1L >= 0 + 0L a__prefix X -> prefix X 0 + 1X >= 0 + 1X a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)) 1 + 0YS + 1X + 0XS + 1Y >= 0 + 0YS + 1X + 0XS + 1Y a__zWadr(nil(), YS) -> nil() 1 + 1YS >= 0 a__zWadr(X1, X2) -> zWadr(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 a__zWadr(XS, nil()) -> nil() 1 + 1XS >= 0 a__from X -> from X 1 + 1X >= 1 + 1X a__from X -> cons(mark X, from s X) 1 + 1X >= 0 + 1X a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)) 0 + 1YS + 1X + 0XS >= 0 + 0YS + 1X + 0XS a__app(nil(), YS) -> mark YS 0 + 1YS >= 0 + 1YS a__app(X1, X2) -> app(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark prefix X -> a__prefix mark X 0 + 1X >= 0 + 1X mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark s X -> s mark X 0 + 1X >= 0 + 1X mark from X -> a__from mark X 1 + 1X >= 1 + 1X mark app(X1, X2) -> a__app(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 mark nil() -> nil() 0 >= 0 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# s X -> mark# X, mark# prefix X -> mark# X, a__app#(nil(), YS) -> mark# YS, a__app#(cons(X, XS), YS) -> mark# X} SCC (8): Strict: { mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# s X -> mark# X, mark# prefix X -> mark# X, a__app#(nil(), YS) -> mark# YS, a__app#(cons(X, XS), YS) -> mark# X} Weak: { mark nil() -> nil(), mark cons(X1, X2) -> cons(mark X1, X2), mark app(X1, X2) -> a__app(mark X1, mark X2), mark from X -> a__from mark X, mark s X -> s mark X, mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2), mark prefix X -> a__prefix mark X, a__app(X1, X2) -> app(X1, X2), a__app(nil(), YS) -> mark YS, a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)), a__from X -> cons(mark X, from s X), a__from X -> from X, a__zWadr(XS, nil()) -> nil(), a__zWadr(X1, X2) -> zWadr(X1, X2), a__zWadr(nil(), YS) -> nil(), a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)), a__prefix X -> prefix X, a__prefix L -> cons(nil(), zWadr(L, prefix L))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__app](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + 1, [app](x0, x1) = x0 + x1, [a__zWadr](x0, x1) = x0 + x1, [zWadr](x0, x1) = x0 + x1, [mark](x0) = x0, [from](x0) = x0 + 1, [s](x0) = x0, [a__from](x0) = x0 + 1, [prefix](x0) = x0 + 1, [a__prefix](x0) = x0 + 1, [nil] = 0, [a__app#](x0, x1) = x0 + x1, [mark#](x0) = x0 Strict: a__app#(cons(X, XS), YS) -> mark# X 1 + 1YS + 1X + 0XS >= 0 + 1X a__app#(nil(), YS) -> mark# YS 0 + 1YS >= 0 + 1YS mark# prefix X -> mark# X 1 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# app(X1, X2) -> a__app#(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# app(X1, X2) -> mark# X2 0 + 1X1 + 1X2 >= 0 + 1X2 mark# app(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 mark# cons(X1, X2) -> mark# X1 1 + 1X1 + 0X2 >= 0 + 1X1 Weak: a__prefix L -> cons(nil(), zWadr(L, prefix L)) 1 + 1L >= 1 + 0L a__prefix X -> prefix X 1 + 1X >= 1 + 1X a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)) 2 + 0YS + 1X + 0XS + 1Y >= 2 + 0YS + 1X + 0XS + 1Y a__zWadr(nil(), YS) -> nil() 0 + 1YS >= 0 a__zWadr(X1, X2) -> zWadr(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 a__zWadr(XS, nil()) -> nil() 0 + 1XS >= 0 a__from X -> from X 1 + 1X >= 1 + 1X a__from X -> cons(mark X, from s X) 1 + 1X >= 1 + 1X a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)) 1 + 1YS + 1X + 0XS >= 1 + 0YS + 1X + 0XS a__app(nil(), YS) -> mark YS 0 + 1YS >= 0 + 1YS a__app(X1, X2) -> app(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark prefix X -> a__prefix mark X 1 + 1X >= 1 + 1X mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark s X -> s mark X 0 + 1X >= 0 + 1X mark from X -> a__from mark X 1 + 1X >= 1 + 1X mark app(X1, X2) -> a__app(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark cons(X1, X2) -> cons(mark X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 mark nil() -> nil() 0 >= 0 SCCS (1): Scc: { mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# s X -> mark# X, a__app#(nil(), YS) -> mark# YS} SCC (5): Strict: { mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__app#(mark X1, mark X2), mark# s X -> mark# X, a__app#(nil(), YS) -> mark# YS} Weak: { mark nil() -> nil(), mark cons(X1, X2) -> cons(mark X1, X2), mark app(X1, X2) -> a__app(mark X1, mark X2), mark from X -> a__from mark X, mark s X -> s mark X, mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2), mark prefix X -> a__prefix mark X, a__app(X1, X2) -> app(X1, X2), a__app(nil(), YS) -> mark YS, a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)), a__from X -> cons(mark X, from s X), a__from X -> from X, a__zWadr(XS, nil()) -> nil(), a__zWadr(X1, X2) -> zWadr(X1, X2), a__zWadr(nil(), YS) -> nil(), a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)), a__prefix X -> prefix X, a__prefix L -> cons(nil(), zWadr(L, prefix L))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = 1, [app](x0, x1) = x0 + x1 + 1, [a__zWadr](x0, x1) = 1, [zWadr](x0, x1) = 1, [mark](x0) = x0, [from](x0) = 1, [s](x0) = x0, [a__from](x0) = 1, [prefix](x0) = 1, [a__prefix](x0) = 1, [nil] = 1, [a__app#](x0, x1) = x0 + x1, [mark#](x0) = x0 Strict: a__app#(nil(), YS) -> mark# YS 1 + 1YS >= 0 + 1YS mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# app(X1, X2) -> a__app#(mark X1, mark X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# app(X1, X2) -> mark# X2 1 + 1X1 + 1X2 >= 0 + 1X2 mark# app(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 Weak: a__prefix L -> cons(nil(), zWadr(L, prefix L)) 1 + 0L >= 1 + 0L a__prefix X -> prefix X 1 + 0X >= 1 + 0X a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)) 1 + 0YS + 0X + 0XS + 0Y >= 1 + 0YS + 0X + 0XS + 0Y a__zWadr(nil(), YS) -> nil() 1 + 0YS >= 1 a__zWadr(X1, X2) -> zWadr(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__zWadr(XS, nil()) -> nil() 1 + 0XS >= 1 a__from X -> from X 1 + 0X >= 1 + 0X a__from X -> cons(mark X, from s X) 1 + 0X >= 1 + 0X a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)) 2 + 1YS + 0X + 0XS >= 1 + 0YS + 0X + 0XS a__app(nil(), YS) -> mark YS 2 + 1YS >= 0 + 1YS a__app(X1, X2) -> app(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark prefix X -> a__prefix mark X 1 + 0X >= 1 + 0X mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> s mark X 0 + 1X >= 0 + 1X mark from X -> a__from mark X 1 + 0X >= 1 + 0X mark app(X1, X2) -> a__app(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark cons(X1, X2) -> cons(mark X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark nil() -> nil() 1 >= 1 SCCS (1): Scc: {mark# s X -> mark# X} SCC (1): Strict: {mark# s X -> mark# X} Weak: { mark nil() -> nil(), mark cons(X1, X2) -> cons(mark X1, X2), mark app(X1, X2) -> a__app(mark X1, mark X2), mark from X -> a__from mark X, mark s X -> s mark X, mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2), mark prefix X -> a__prefix mark X, a__app(X1, X2) -> app(X1, X2), a__app(nil(), YS) -> mark YS, a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)), a__from X -> cons(mark X, from s X), a__from X -> from X, a__zWadr(XS, nil()) -> nil(), a__zWadr(X1, X2) -> zWadr(X1, X2), a__zWadr(nil(), YS) -> nil(), a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)), a__prefix X -> prefix X, a__prefix L -> cons(nil(), zWadr(L, prefix L))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__app](x0, x1) = 0, [cons](x0, x1) = 1, [app](x0, x1) = 1, [a__zWadr](x0, x1) = 0, [zWadr](x0, x1) = 1, [mark](x0) = x0 + 1, [from](x0) = 1, [s](x0) = x0 + 1, [a__from](x0) = x0 + 1, [prefix](x0) = 1, [a__prefix](x0) = x0 + 1, [nil] = 1, [mark#](x0) = x0 + 1 Strict: mark# s X -> mark# X 2 + 1X >= 1 + 1X Weak: a__prefix L -> cons(nil(), zWadr(L, prefix L)) 1 + 1L >= 1 + 0L a__prefix X -> prefix X 1 + 1X >= 1 + 0X a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)) 0 + 0YS + 0X + 0XS + 0Y >= 1 + 0YS + 0X + 0XS + 0Y a__zWadr(nil(), YS) -> nil() 0 + 0YS >= 1 a__zWadr(X1, X2) -> zWadr(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__zWadr(XS, nil()) -> nil() 0 + 0XS >= 1 a__from X -> from X 1 + 1X >= 1 + 0X a__from X -> cons(mark X, from s X) 1 + 1X >= 1 + 0X a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)) 0 + 0YS + 0X + 0XS >= 1 + 0YS + 0X + 0XS a__app(nil(), YS) -> mark YS 0 + 0YS >= 1 + 1YS a__app(X1, X2) -> app(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark prefix X -> a__prefix mark X 2 + 0X >= 2 + 1X mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark s X -> s mark X 2 + 1X >= 2 + 1X mark from X -> a__from mark X 2 + 0X >= 2 + 1X mark app(X1, X2) -> a__app(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark cons(X1, X2) -> cons(mark X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark nil() -> nil() 2 >= 1 Qed