YES(?,ELEMENTARY) 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: YES(?,ELEMENTARY) Input Problem: innermost runtime-complexity with respect to Rules: { app(nil(), YS) -> YS , app(cons(X), YS) -> cons(X) , from(X) -> cons(X) , zWadr(nil(), YS) -> nil() , zWadr(XS, nil()) -> nil() , zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X))) , prefix(L) -> cons(nil())} Proof Output: Strict Rules in Predicative Notation: { app(; nil(), YS) -> YS , app(; cons(; X), YS) -> cons(; X) , from(X;) -> cons(; X) , zWadr(YS; nil()) -> nil() , zWadr(nil(); XS) -> nil() , zWadr(cons(; Y); cons(; X)) -> cons(; app(; Y, cons(; X))) , prefix(; L) -> cons(; nil())} Safe Mapping: safe(app) = {1, 2}, safe(nil) = {}, safe(cons) = {1}, safe(from) = {}, safe(zWadr) = {1}, safe(prefix) = {1} Argument Permutation: mu(app) = [2, 1], mu(from) = [1], mu(zWadr) = [1, 2], mu(prefix) = [1] Precedence: prefix ~ prefix, prefix > from, zWadr > prefix, zWadr ~ zWadr, zWadr > from, zWadr > app, from ~ from, app > prefix, app > from, app ~ app