YES(?,O(n^1)) * Step 1: FromIts WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalfstart(A,B) -> evalfentryin(A,B) True (1,1) 1. evalfentryin(A,B) -> evalfbb1in(B,A) True (?,1) 2. evalfbb1in(A,B) -> evalfbbin(A,B) [A >= B] (?,1) 3. evalfbb1in(A,B) -> evalfreturnin(A,B) [B >= 1 + A] (?,1) 4. evalfbbin(A,B) -> evalfbb1in(A,1 + B) [A + -1*B >= 0] (?,1) 5. evalfreturnin(A,B) -> evalfstop(A,B) [-1 + -1*A + B >= 0] (?,1) Signature: {(evalfbb1in,2);(evalfbbin,2);(evalfentryin,2);(evalfreturnin,2);(evalfstart,2);(evalfstop,2)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{5},4->{2,3},5->{}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalfstart(A,B) -> evalfentryin(A,B) True evalfentryin(A,B) -> evalfbb1in(B,A) True evalfbb1in(A,B) -> evalfbbin(A,B) [A >= B] evalfbb1in(A,B) -> evalfreturnin(A,B) [B >= 1 + A] evalfbbin(A,B) -> evalfbb1in(A,1 + B) [A + -1*B >= 0] evalfreturnin(A,B) -> evalfstop(A,B) [-1 + -1*A + B >= 0] Signature: {(evalfbb1in,2);(evalfbbin,2);(evalfentryin,2);(evalfreturnin,2);(evalfstart,2);(evalfstop,2)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{5},4->{2,3},5->{}] + Applied Processor: AddSinks + Details: () * Step 3: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalfstart(A,B) -> evalfentryin(A,B) True evalfentryin(A,B) -> evalfbb1in(B,A) True evalfbb1in(A,B) -> evalfbbin(A,B) [A >= B] evalfbb1in(A,B) -> evalfreturnin(A,B) [B >= 1 + A] evalfbbin(A,B) -> evalfbb1in(A,1 + B) [A + -1*B >= 0] evalfreturnin(A,B) -> evalfstop(A,B) [-1 + -1*A + B >= 0] evalfstop(A,B) -> exitus616(A,B) True Signature: {(evalfbb1in,2) ;(evalfbbin,2) ;(evalfentryin,2) ;(evalfreturnin,2) ;(evalfstart,2) ;(evalfstop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{5},4->{2,3},5->{6}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6] | `- p:[2,4] c: [2,4] * Step 4: AbstractSize WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: evalfstart(A,B) -> evalfentryin(A,B) True evalfentryin(A,B) -> evalfbb1in(B,A) True evalfbb1in(A,B) -> evalfbbin(A,B) [A >= B] evalfbb1in(A,B) -> evalfreturnin(A,B) [B >= 1 + A] evalfbbin(A,B) -> evalfbb1in(A,1 + B) [A + -1*B >= 0] evalfreturnin(A,B) -> evalfstop(A,B) [-1 + -1*A + B >= 0] evalfstop(A,B) -> exitus616(A,B) True Signature: {(evalfbb1in,2) ;(evalfbbin,2) ;(evalfentryin,2) ;(evalfreturnin,2) ;(evalfstart,2) ;(evalfstop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{5},4->{2,3},5->{6}] ,We construct a looptree: P: [0,1,2,3,4,5,6] | `- p:[2,4] c: [2,4]) + Applied Processor: AbstractSize Minimize + Details: () * Step 5: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,0.0] evalfstart ~> evalfentryin [A <= A, B <= B] evalfentryin ~> evalfbb1in [A <= B, B <= A] evalfbb1in ~> evalfbbin [A <= A, B <= B] evalfbb1in ~> evalfreturnin [A <= A, B <= B] evalfbbin ~> evalfbb1in [A <= A, B <= K + B] evalfreturnin ~> evalfstop [A <= A, B <= B] evalfstop ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= A + B] evalfbb1in ~> evalfbbin [A <= A, B <= B] evalfbbin ~> evalfbb1in [A <= A, B <= K + B] + Applied Processor: AbstractFlow + Details: () * Step 6: Lare WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0] evalfstart ~> evalfentryin [] evalfentryin ~> evalfbb1in [A ~=> B,B ~=> A] evalfbb1in ~> evalfbbin [] evalfbb1in ~> evalfreturnin [] evalfbbin ~> evalfbb1in [B ~+> B,K ~+> B] evalfreturnin ~> evalfstop [] evalfstop ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] evalfbb1in ~> evalfbbin [] evalfbbin ~> evalfbb1in [B ~+> B,K ~+> B] + Applied Processor: Lare + Details: evalfstart ~> exitus616 [A ~=> B ,B ~=> A ,A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B] + evalfbb1in> [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,O(n^1))