YES(?,O(1)) * Step 1: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evalndloopstart(A) -> evalndloopentryin(A) True (1,1) 1. evalndloopentryin(A) -> evalndloopbbin(0) True (?,1) 2. evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] (?,1) 3. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] (?,1) 4. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] (?,1) 5. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] (?,1) 6. evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] (?,1) Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Flow Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: evalndloopstart(A) -> evalndloopentryin(A) True evalndloopentryin(A) -> evalndloopbbin(0) True evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Rule Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] + Applied Processor: AddSinks + Details: () * Step 3: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: evalndloopstart(A) -> evalndloopentryin(A) True evalndloopentryin(A) -> evalndloopbbin(0) True evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] evalndloopstop(A) -> exitus616(A) True evalndloopstop(A) -> exitus616(A) True evalndloopstop(A) -> exitus616(A) True Signature: {(evalndloopbbin,1) ;(evalndloopentryin,1) ;(evalndloopreturnin,1) ;(evalndloopstart,1) ;(evalndloopstop,1) ;(exitus616,1)} Rule Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{7,8,9}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[2] c: [2] * Step 4: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: evalndloopstart(A) -> evalndloopentryin(A) True evalndloopentryin(A) -> evalndloopbbin(0) True evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] evalndloopstop(A) -> exitus616(A) True evalndloopstop(A) -> exitus616(A) True evalndloopstop(A) -> exitus616(A) True Signature: {(evalndloopbbin,1) ;(evalndloopentryin,1) ;(evalndloopreturnin,1) ;(evalndloopstart,1) ;(evalndloopstop,1) ;(exitus616,1)} Rule Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{7,8,9}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[2] c: [2]) + Applied Processor: AbstractSize Minimize + Details: () * Step 5: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,0.0] evalndloopstart ~> evalndloopentryin [A <= A] evalndloopentryin ~> evalndloopbbin [A <= 0*K] evalndloopbbin ~> evalndloopbbin [A <= 9*K] evalndloopbbin ~> evalndloopreturnin [A <= A] evalndloopbbin ~> evalndloopreturnin [A <= A] evalndloopbbin ~> evalndloopreturnin [A <= A] evalndloopreturnin ~> evalndloopstop [A <= A] evalndloopstop ~> exitus616 [A <= A] evalndloopstop ~> exitus616 [A <= A] evalndloopstop ~> exitus616 [A <= A] + Loop: [0.0 <= 8*K + A] evalndloopbbin ~> evalndloopbbin [A <= 9*K] + Applied Processor: AbstractFlow + Details: () * Step 6: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,0.0] evalndloopstart ~> evalndloopentryin [] evalndloopentryin ~> evalndloopbbin [K ~=> A] evalndloopbbin ~> evalndloopbbin [K ~=> A] evalndloopbbin ~> evalndloopreturnin [] evalndloopbbin ~> evalndloopreturnin [] evalndloopbbin ~> evalndloopreturnin [] evalndloopreturnin ~> evalndloopstop [] evalndloopstop ~> exitus616 [] evalndloopstop ~> exitus616 [] evalndloopstop ~> exitus616 [] + Loop: [A ~+> 0.0,K ~*> 0.0] evalndloopbbin ~> evalndloopbbin [K ~=> A] + Applied Processor: Lare + Details: evalndloopstart ~> exitus616 [K ~=> A,tick ~+> tick,K ~+> 0.0,K ~+> tick,K ~*> 0.0,K ~*> tick] + evalndloopbbin> [K ~=> A,A ~+> 0.0,A ~+> tick,tick ~+> tick,K ~*> 0.0,K ~*> tick] YES(?,O(1))