YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (1,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (1,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (?,1) 12. evalNestedMultiplereturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5) ;(exitus616,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11,12},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{} ,12->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,10,4,9,6,5,7,8] c: [2] | `- p:[5,9,6,7] c: [5] * Step 4: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (?,1) 12. evalNestedMultiplereturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5) ;(exitus616,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11,12},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{} ,12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,10,4,9,6,5,7,8] c: [2] | `- p:[5,9,6,7] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.0.0] evalNestedMultiplestart ~> evalNestedMultipleentryin [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultipleentryin ~> evalNestedMultiplebb5in [A <= B, B <= A, C <= D, D <= C, E <= E] evalNestedMultiplebb5in ~> evalNestedMultiplebb2in [A <= A, B <= B, C <= C, D <= D, E <= D] evalNestedMultiplebb5in ~> evalNestedMultiplereturnin [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb2in ~> evalNestedMultiplebb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb2in ~> evalNestedMultiplebb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb3in ~> evalNestedMultiplebb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb1in ~> evalNestedMultiplebb2in [A <= A, B <= B, C <= C, D <= D, E <= K + E] evalNestedMultiplebb4in ~> evalNestedMultiplebb5in [A <= A, B <= K + B, C <= C, D <= E, E <= E] evalNestedMultiplereturnin ~> evalNestedMultiplestop [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplereturnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= 2*K + A + B] evalNestedMultiplebb5in ~> evalNestedMultiplebb2in [A <= A, B <= B, C <= C, D <= D, E <= D] evalNestedMultiplebb4in ~> evalNestedMultiplebb5in [A <= A, B <= K + B, C <= C, D <= E, E <= E] evalNestedMultiplebb2in ~> evalNestedMultiplebb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb1in ~> evalNestedMultiplebb2in [A <= A, B <= B, C <= C, D <= D, E <= K + E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb2in ~> evalNestedMultiplebb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb3in ~> evalNestedMultiplebb4in [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0.0 <= 2*K + C + E] evalNestedMultiplebb2in ~> evalNestedMultiplebb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb1in ~> evalNestedMultiplebb2in [A <= A, B <= B, C <= C, D <= D, E <= K + E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [A <= A, B <= B, C <= C, D <= D, E <= E] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.0.0] evalNestedMultiplestart ~> evalNestedMultipleentryin [] evalNestedMultipleentryin ~> evalNestedMultiplebb5in [A ~=> B,B ~=> A,C ~=> D,D ~=> C] evalNestedMultiplebb5in ~> evalNestedMultiplebb2in [D ~=> E] evalNestedMultiplebb5in ~> evalNestedMultiplereturnin [] evalNestedMultiplebb2in ~> evalNestedMultiplebb4in [] evalNestedMultiplebb2in ~> evalNestedMultiplebb3in [] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [] evalNestedMultiplebb3in ~> evalNestedMultiplebb4in [] evalNestedMultiplebb1in ~> evalNestedMultiplebb2in [E ~+> E,K ~+> E] evalNestedMultiplebb4in ~> evalNestedMultiplebb5in [E ~=> D,B ~+> B,K ~+> B] evalNestedMultiplereturnin ~> evalNestedMultiplestop [] evalNestedMultiplereturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] evalNestedMultiplebb5in ~> evalNestedMultiplebb2in [D ~=> E] evalNestedMultiplebb4in ~> evalNestedMultiplebb5in [E ~=> D,B ~+> B,K ~+> B] evalNestedMultiplebb2in ~> evalNestedMultiplebb4in [] evalNestedMultiplebb1in ~> evalNestedMultiplebb2in [E ~+> E,K ~+> E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [] evalNestedMultiplebb2in ~> evalNestedMultiplebb3in [] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [] evalNestedMultiplebb3in ~> evalNestedMultiplebb4in [] + Loop: [C ~+> 0.0.0,E ~+> 0.0.0,K ~*> 0.0.0] evalNestedMultiplebb2in ~> evalNestedMultiplebb3in [] evalNestedMultiplebb1in ~> evalNestedMultiplebb2in [E ~+> E,K ~+> E] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [] evalNestedMultiplebb3in ~> evalNestedMultiplebb1in [] + Applied Processor: LareProcessor + Details: evalNestedMultiplestart ~> exitus616 [A ~=> B ,B ~=> A ,C ~=> D ,C ~=> E ,D ~=> C ,A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,C ~+> D ,C ~+> E ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> D ,C ~*> E ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> E ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> E ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> D ,K ~^> E ,K ~^> 0.0.0 ,K ~^> tick] evalNestedMultiplestart ~> evalNestedMultiplestop [A ~=> B ,B ~=> A ,C ~=> D ,C ~=> E ,D ~=> C ,A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,C ~+> D ,C ~+> E ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> D ,C ~*> E ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> E ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> E ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> D ,K ~^> E ,K ~^> 0.0.0 ,K ~^> tick] + evalNestedMultiplebb5in> [D ~=> E ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> E ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> D ,C ~*> E ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> E ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> E ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> D ,K ~^> E ,K ~^> 0.0.0 ,K ~^> tick] + evalNestedMultiplebb3in> [C ~+> 0.0.0 ,C ~+> tick ,E ~+> E ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> E ,C ~*> E ,E ~*> E ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick] evalNestedMultiplebb2in> [C ~+> 0.0.0 ,C ~+> tick ,E ~+> E ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> E ,C ~*> E ,E ~*> E ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick] YES(?,PRIMREC)