MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() quote(n__0()) -> 01() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) quote1(n__nil()) -> nil1() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0,n__s/1,n__sel/2,nil1/0,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,cons,fcons,first,first1,from,nil,quote,quote1 ,s,sel,sel1,unquote,unquote1} and constructors {01,cons1,n__0,n__cons,n__first,n__from,n__nil,n__s,n__sel ,nil1,s1} + Applied Processor: NaturalPI {shape = Mixed 3, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: Incompatible MAYBE