* Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) - Signature: {first/2,from/1} / {0/0,cons/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {first,from} and constructors {0,cons,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) - Signature: {first/2,from/1} / {0/0,cons/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {first,from} and constructors {0,cons,nil,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs first#(0(),X) -> c_1() first#(s(X),cons(Y)) -> c_2() from#(X) -> c_3() Weak DPs and mark the set of starting terms. * Step 3: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: first#(0(),X) -> c_1() first#(s(X),cons(Y)) -> c_2() from#(X) -> c_3() - Weak TRS: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) - Signature: {first/2,from/1,first#/2,from#/1} / {0/0,cons/1,nil/0,s/1,c_1/0,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {first#,from#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: first#(0(),X) -> c_1() first#(s(X),cons(Y)) -> c_2() from#(X) -> c_3() * Step 4: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: first#(0(),X) -> c_1() first#(s(X),cons(Y)) -> c_2() from#(X) -> c_3() - Signature: {first/2,from/1,first#/2,from#/1} / {0/0,cons/1,nil/0,s/1,c_1/0,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {first#,from#} and constructors {0,cons,nil,s} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:first#(0(),X) -> c_1() 2:S:first#(s(X),cons(Y)) -> c_2() 3:S:from#(X) -> c_3() The dependency graph contains no loops, we remove all dependency pairs. * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {first/2,from/1,first#/2,from#/1} / {0/0,cons/1,nil/0,s/1,c_1/0,c_2/0,c_3/0} - Obligation: innermost runtime complexity wrt. defined symbols {first#,from#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))