WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(cons(x,k),l) -> g(k,l,cons(x,k)) f(empty(),l) -> l g(a,b,c) -> f(a,cons(b,c)) - Signature: {f/2,g/3} / {cons/2,empty/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {cons,empty} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(cons(x,k),l) -> g(k,l,cons(x,k)) f(empty(),l) -> l g(a,b,c) -> f(a,cons(b,c)) - Signature: {f/2,g/3} / {cons/2,empty/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {cons,empty} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: none Following symbols are considered usable: {f,g} TcT has computed the following interpretation: p(cons) = [0] p(empty) = [0] p(f) = [2] x2 + [11] p(g) = [11] Following rules are strictly oriented: f(empty(),l) = [2] l + [11] > [1] l + [0] = l Following rules are (at-least) weakly oriented: f(cons(x,k),l) = [2] l + [11] >= [11] = g(k,l,cons(x,k)) g(a,b,c) = [11] >= [11] = f(a,cons(b,c)) * Step 3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(cons(x,k),l) -> g(k,l,cons(x,k)) g(a,b,c) -> f(a,cons(b,c)) - Weak TRS: f(empty(),l) -> l - Signature: {f/2,g/3} / {cons/2,empty/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {cons,empty} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- cons :: ["A"(14) x "A"(14)] -(14)-> "A"(14) cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) empty :: [] -(0)-> "A"(14) f :: ["A"(14) x "A"(0)] -(3)-> "A"(0) g :: ["A"(14) x "A"(0) x "A"(0)] -(4)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "empty_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: g(a,b,c) -> f(a,cons(b,c)) 2. Weak: f(cons(x,k),l) -> g(k,l,cons(x,k)) * Step 4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(cons(x,k),l) -> g(k,l,cons(x,k)) - Weak TRS: f(empty(),l) -> l g(a,b,c) -> f(a,cons(b,c)) - Signature: {f/2,g/3} / {cons/2,empty/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {cons,empty} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- cons :: ["A"(0) x "A"(10)] -(10)-> "A"(10) cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) empty :: [] -(0)-> "A"(10) f :: ["A"(10) x "A"(0)] -(8)-> "A"(0) g :: ["A"(10) x "A"(0) x "A"(0)] -(11)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "empty_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: f(cons(x,k),l) -> g(k,l,cons(x,k)) 2. Weak: WORST_CASE(?,O(n^1))