WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(0()) -> cons(0()) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() - Signature: {f/1,p/1} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,p} and constructors {0,cons,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. MAYBE + Considered Problem: - Strict TRS: f(0()) -> cons(0()) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() - Signature: {f/1,p/1} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,p} and constructors {0,cons,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: Ara. MAYBE + Considered Problem: - Strict TRS: f(0()) -> cons(0()) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() - Signature: {f/1,p/1} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,p} and constructors {0,cons,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 3, araTimeout = 15, araRuleShifting = Just 1, isBestCase = True, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(0, 0, 0) F (TrsFun "0") :: [] -(0)-> "A"(2, 2, 1) F (TrsFun "cons") :: ["A"(0, 0, 0)] -(0)-> "A"(0, 0, 0) F (TrsFun "f") :: ["A"(0, 0, 0)] -(1)-> "A"(0, 0, 0) F (TrsFun "main") :: ["A"(0, 0, 1)] -(1)-> "A"(0, 0, 0) F (TrsFun "p") :: ["A"(1, 1, 1)] -(0)-> "A"(0, 0, 0) F (TrsFun "s") :: ["A"(0, 0, 0)] -(0)-> "A"(0, 0, 0) F (TrsFun "s") :: ["A"(2, 2, 1)] -(1)-> "A"(1, 1, 1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: f(0()) -> cons(0()) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() main(x1) -> p(x1) 2. Weak: ** Step 1.b:1: Bounds. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(0()) -> cons(0()) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() - Signature: {f/1,p/1} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,p} and constructors {0,cons,s} + Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} + Details: The problem is match-bounded by 2. The enriched problem is compatible with follwoing automaton. 0_0() -> 2 0_1() -> 1 0_1() -> 3 0_2() -> 4 cons_0(2) -> 2 cons_1(3) -> 1 cons_2(4) -> 1 f_0(2) -> 1 f_1(4) -> 1 p_0(2) -> 1 p_1(5) -> 4 s_0(2) -> 2 s_1(3) -> 5 ** Step 1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(0()) -> cons(0()) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() - Signature: {f/1,p/1} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,p} and constructors {0,cons,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))