YES(?,PRIMREC) * Step 1: FromIts MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True (?,1) 2. evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] (?,1) 3. evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True (?,1) 5. evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] (?,1) 6. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] (?,1) 7. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] (?,1) 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True (?,1) 10. evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True (?,1) 11. evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True (?,1) 12. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1) Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{12},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks MAYBE + Considered Problem: Rules: evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{12},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{}] + Applied Processor: AddSinks + Details: () * Step 3: Decompose MAYBE + Considered Problem: Rules: evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True evalfstop(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4) ;(exitus616,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{12},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{13}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[2,11,5,4,10,7,6,8,9] c: [2,4,5,9,11] | `- p:[6,10,7,8] c: [6,7,8,10] * Step 4: AbstractSize MAYBE + Considered Problem: (Rules: evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True evalfstop(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4) ;(exitus616,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{12},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{13}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[2,11,5,4,10,7,6,8,9] c: [2,4,5,9,11] | `- p:[6,10,7,8] c: [6,7,8,10]) + Applied Processor: AbstractSize Minimize + Details: () * Step 5: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalfstart ~> evalfentryin [A <= A, B <= B, C <= C, D <= D] evalfentryin ~> evalfbb5in [A <= B, B <= B, C <= C, D <= D] evalfbb5in ~> evalfbbin [A <= A, B <= B, C <= C, D <= D] evalfbb5in ~> evalfreturnin [A <= A, B <= B, C <= C, D <= D] evalfbbin ~> evalfbb2in [A <= A, B <= B, C <= K + B, D <= K + A + B] evalfbb2in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] evalfbb2in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] evalfbb1in ~> evalfbb2in [A <= A, B <= B, C <= C, D <= K + D] evalfbb4in ~> evalfbb5in [A <= K + C + D, B <= K + C, C <= C, D <= D] evalfreturnin ~> evalfstop [A <= A, B <= B, C <= C, D <= D] evalfstop ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + B] evalfbb5in ~> evalfbbin [A <= A, B <= B, C <= C, D <= D] evalfbb4in ~> evalfbb5in [A <= K + C + D, B <= K + C, C <= C, D <= D] evalfbb2in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] evalfbbin ~> evalfbb2in [A <= A, B <= B, C <= K + B, D <= K + A + B] evalfbb1in ~> evalfbb2in [A <= A, B <= B, C <= C, D <= K + D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb2in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + C + D] evalfbb2in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D] evalfbb1in ~> evalfbb2in [A <= A, B <= B, C <= C, D <= K + D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] + Applied Processor: AbstractFlow + Details: () * Step 6: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalfstart ~> evalfentryin [] evalfentryin ~> evalfbb5in [B ~=> A] evalfbb5in ~> evalfbbin [] evalfbb5in ~> evalfreturnin [] evalfbbin ~> evalfbb2in [A ~+> D,B ~+> C,B ~+> D,K ~+> C,K ~+> D] evalfbb2in ~> evalfbb4in [] evalfbb2in ~> evalfbb3in [] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb4in [] evalfbb1in ~> evalfbb2in [D ~+> D,K ~+> D] evalfbb4in ~> evalfbb5in [C ~+> A,C ~+> B,D ~+> A,K ~+> A,K ~+> B] evalfreturnin ~> evalfstop [] evalfstop ~> exitus616 [] + Loop: [B ~+> 0.0,K ~+> 0.0] evalfbb5in ~> evalfbbin [] evalfbb4in ~> evalfbb5in [C ~+> A,C ~+> B,D ~+> A,K ~+> A,K ~+> B] evalfbb2in ~> evalfbb4in [] evalfbbin ~> evalfbb2in [A ~+> D,B ~+> C,B ~+> D,K ~+> C,K ~+> D] evalfbb1in ~> evalfbb2in [D ~+> D,K ~+> D] evalfbb3in ~> evalfbb1in [] evalfbb2in ~> evalfbb3in [] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb4in [] + Loop: [C ~+> 0.0.0,D ~+> 0.0.0,K ~+> 0.0.0] evalfbb2in ~> evalfbb3in [] evalfbb1in ~> evalfbb2in [D ~+> D,K ~+> D] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb1in [] + Applied Processor: Lare + Details: evalfstart ~> exitus616 [B ~=> A ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> A ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + evalfbb5in> [A ~+> A ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> A ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + evalfbb3in> [C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> D ,D ~*> D ,K ~*> D] evalfbb2in> [C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> D ,D ~*> D ,K ~*> D] YES(?,PRIMREC)