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