WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () *** Step 1.a:1.a:1: Decompose. MAYBE + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: Decompose {onSelection = any filtered on not main function of strict-rules, withBound = BestCaseLBMax} + Details: We analyse the complexity of following sub-problems (R) and (S). For the best-case lower bound analysis the maximum derivation length of either sub-problem provides a lower bound in terms of derivation length of the original TRS. Problem (R) - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Weak TRS: main(x1) -> fold#3(x1) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} Problem (S) - Strict TRS: main(x1) -> fold#3(x1) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} **** Step 1.a:1.a:1.a:1: Ara. MAYBE + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Weak TRS: main(x1) -> fold#3(x1) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,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) F (TrsFun "Cons") :: ["A"(0) x "A"(1)] -(1)-> "A"(1) F (TrsFun "Nil") :: [] -(0)-> "A"(1) F (TrsFun "S") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "fold#3") :: ["A"(1)] -(1)-> "A"(0) F (TrsFun "main") :: ["A"(1)] -(0)-> "A"(0) F (TrsFun "plus#2") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) 2. Weak: **** Step 1.a:1.a:1.b:1: Ara. MAYBE + Considered Problem: - Strict TRS: main(x1) -> fold#3(x1) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: Ara {minDegree = 1, maxDegree = 3, araTimeout = 15, araRuleShifting = Just 1, isBestCase = True, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "fold#3") :: ["A"(0, 0, 1)] -(0)-> "A"(0, 0, 0) F (TrsFun "main") :: ["A"(0, 0, 1)] -(1)-> "A"(0, 0, 0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: main(x1) -> fold#3(x1) 2. Weak: *** Step 1.a:1.b:1: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: fold#3(y){y -> Cons(x,y)} = fold#3(Cons(x,y)) ->^+ plus#2(x,fold#3(y)) = C[fold#3(y) = fold#3(y){}] ** Step 1.b:1: Bounds. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} + Details: The problem is match-bounded by 1. The enriched problem is compatible with follwoing automaton. 0_0() -> 1 0_0() -> 2 0_0() -> 4 0_1() -> 1 0_1() -> 3 Cons_0(2,2) -> 1 Cons_0(2,2) -> 2 Cons_0(2,2) -> 4 Nil_0() -> 1 Nil_0() -> 2 Nil_0() -> 4 S_0(2) -> 1 S_0(2) -> 2 S_0(2) -> 4 S_1(1) -> 1 S_1(3) -> 1 S_1(3) -> 3 S_1(4) -> 1 S_1(4) -> 4 fold#3_0(2) -> 1 fold#3_1(2) -> 1 fold#3_1(2) -> 3 main_0(2) -> 1 plus#2_0(2,2) -> 1 plus#2_1(2,2) -> 4 plus#2_1(2,3) -> 1 plus#2_1(2,3) -> 3 2 -> 1 2 -> 4 3 -> 1 ** Step 1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {fold#3,main,plus#2} and constructors {0,Cons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))