* Step 1: Sum WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: fcons(X,Z) -> cons(X,Z) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z)) from(X) -> cons(X,from(s(X))) quote(0()) -> 01() quote(s(X)) -> s1(quote(X)) quote(sel(X,Z)) -> sel1(X,Z) quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z)) quote1(first(X,Z)) -> first1(X,Z) quote1(nil()) -> nil1() sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1} / {0/0,01/0,cons/2 ,cons1/2,nil/0,nil1/0,s/1,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {fcons,first,first1,from,quote,quote1,sel,sel1,unquote ,unquote1} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: fcons(X,Z) -> cons(X,Z) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z)) from(X) -> cons(X,from(s(X))) quote(0()) -> 01() quote(s(X)) -> s1(quote(X)) quote(sel(X,Z)) -> sel1(X,Z) quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z)) quote1(first(X,Z)) -> first1(X,Z) quote1(nil()) -> nil1() sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,Z) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {fcons/2,first/2,first1/2,from/1,quote/1,quote1/1,sel/2,sel1/2,unquote/1,unquote1/1} / {0/0,01/0,cons/2 ,cons1/2,nil/0,nil1/0,s/1,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {fcons,first,first1,from,quote,quote1,sel,sel1,unquote ,unquote1} and constructors {0,01,cons,cons1,nil,nil1,s,s1} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: first(x,z){x -> s(x),z -> cons(y,z)} = first(s(x),cons(y,z)) ->^+ cons(y,first(x,z)) = C[first(x,z) = first(x,z){}] WORST_CASE(Omega(n^1),?)