MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalspeedpldi2start(A,B,C) -> evalspeedpldi2entryin(A,B,C) True (1,1) 1. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2bb5in(B,0,A) [A >= 0 && B >= 1] (?,1) 2. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= 1 + A] (?,1) 3. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= B] (?,1) 4. evalspeedpldi2bb5in(A,B,C) -> evalspeedpldi2bb2in(A,B,C) [C >= 1] (?,1) 5. evalspeedpldi2bb5in(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= C] (?,1) 6. evalspeedpldi2bb2in(A,B,C) -> evalspeedpldi2bb3in(A,B,C) [A >= 1 + B] (?,1) 7. evalspeedpldi2bb2in(A,B,C) -> evalspeedpldi2bb5in(A,0,C) [B >= A] (?,1) 8. evalspeedpldi2bb3in(A,B,C) -> evalspeedpldi2bb5in(A,1 + B,-1 + C) True (?,1) 9. evalspeedpldi2returnin(A,B,C) -> evalspeedpldi2stop(A,B,C) True (?,1) Signature: {(evalspeedpldi2bb2in,3) ;(evalspeedpldi2bb3in,3) ;(evalspeedpldi2bb5in,3) ;(evalspeedpldi2entryin,3) ;(evalspeedpldi2returnin,3) ;(evalspeedpldi2start,3) ;(evalspeedpldi2stop,3)} Flow Graph: [0->{1,2,3},1->{4,5},2->{9},3->{9},4->{6,7},5->{9},6->{8},7->{4,5},8->{4,5},9->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. evalspeedpldi2start(A,B,C) -> evalspeedpldi2entryin(A,B,C) True (1,1) 1. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2bb5in(B,0,A) [A >= 0 && B >= 1] (1,1) 2. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= 1 + A] (1,1) 3. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= B] (1,1) 4. evalspeedpldi2bb5in(A,B,C) -> evalspeedpldi2bb2in(A,B,C) [C >= 1] (?,1) 5. evalspeedpldi2bb5in(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= C] (1,1) 6. evalspeedpldi2bb2in(A,B,C) -> evalspeedpldi2bb3in(A,B,C) [A >= 1 + B] (?,1) 7. evalspeedpldi2bb2in(A,B,C) -> evalspeedpldi2bb5in(A,0,C) [B >= A] (?,1) 8. evalspeedpldi2bb3in(A,B,C) -> evalspeedpldi2bb5in(A,1 + B,-1 + C) True (?,1) 9. evalspeedpldi2returnin(A,B,C) -> evalspeedpldi2stop(A,B,C) True (1,1) Signature: {(evalspeedpldi2bb2in,3) ;(evalspeedpldi2bb3in,3) ;(evalspeedpldi2bb5in,3) ;(evalspeedpldi2entryin,3) ;(evalspeedpldi2returnin,3) ;(evalspeedpldi2start,3) ;(evalspeedpldi2stop,3)} Flow Graph: [0->{1,2,3},1->{4,5},2->{9},3->{9},4->{6,7},5->{9},6->{8},7->{4,5},8->{4,5},9->{}] + Applied Processor: AddSinks + Details: () * Step 3: Failure MAYBE + Considered Problem: Rules: 0. evalspeedpldi2start(A,B,C) -> evalspeedpldi2entryin(A,B,C) True (1,1) 1. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2bb5in(B,0,A) [A >= 0 && B >= 1] (?,1) 2. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= 1 + A] (?,1) 3. evalspeedpldi2entryin(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= B] (?,1) 4. evalspeedpldi2bb5in(A,B,C) -> evalspeedpldi2bb2in(A,B,C) [C >= 1] (?,1) 5. evalspeedpldi2bb5in(A,B,C) -> evalspeedpldi2returnin(A,B,C) [0 >= C] (?,1) 6. evalspeedpldi2bb2in(A,B,C) -> evalspeedpldi2bb3in(A,B,C) [A >= 1 + B] (?,1) 7. evalspeedpldi2bb2in(A,B,C) -> evalspeedpldi2bb5in(A,0,C) [B >= A] (?,1) 8. evalspeedpldi2bb3in(A,B,C) -> evalspeedpldi2bb5in(A,1 + B,-1 + C) True (?,1) 9. evalspeedpldi2returnin(A,B,C) -> evalspeedpldi2stop(A,B,C) True (?,1) 10. evalspeedpldi2returnin(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(evalspeedpldi2bb2in,3) ;(evalspeedpldi2bb3in,3) ;(evalspeedpldi2bb5in,3) ;(evalspeedpldi2entryin,3) ;(evalspeedpldi2returnin,3) ;(evalspeedpldi2start,3) ;(evalspeedpldi2stop,3) ;(exitus616,3)} Flow Graph: [0->{1,2,3},1->{4,5},2->{9,10},3->{9,10},4->{6,7},5->{9,10},6->{8},7->{4,5},8->{4,5},9->{},10->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | `- p:[4,7,8,6] c: [] MAYBE