YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E) -> f12(1 + A,B,C,D,E) [A >= 0 && 9 >= A] (?,1) 1. f25(A,B,C,D,E) -> f25(A,1 + B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && 9 >= B] (?,1) 2. f25(A,B,C,D,E) -> f36(A,B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && B >= 10] (?,1) 3. f12(A,B,C,D,E) -> f25(A,0,F,D,E) [A >= 0 && A >= 10] (?,1) 4. f0(A,B,C,D,E) -> f12(0,B,C,F,G) True (1,1) Signature: {(f0,5);(f12,5);(f25,5);(f36,5)} Flow Graph: [0->{0,3},1->{1,2},2->{},3->{1,2},4->{0,3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E) -> f12(1 + A,B,C,D,E) [A >= 0 && 9 >= A] (?,1) 1. f25(A,B,C,D,E) -> f25(A,1 + B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && 9 >= B] (?,1) 2. f25(A,B,C,D,E) -> f36(A,B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && B >= 10] (1,1) 3. f12(A,B,C,D,E) -> f25(A,0,F,D,E) [A >= 0 && A >= 10] (1,1) 4. f0(A,B,C,D,E) -> f12(0,B,C,F,G) True (1,1) Signature: {(f0,5);(f12,5);(f25,5);(f36,5)} Flow Graph: [0->{0,3},1->{1,2},2->{},3->{1,2},4->{0,3}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,2),(4,3)] * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E) -> f12(1 + A,B,C,D,E) [A >= 0 && 9 >= A] (?,1) 1. f25(A,B,C,D,E) -> f25(A,1 + B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && 9 >= B] (?,1) 2. f25(A,B,C,D,E) -> f36(A,B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && B >= 10] (1,1) 3. f12(A,B,C,D,E) -> f25(A,0,F,D,E) [A >= 0 && A >= 10] (1,1) 4. f0(A,B,C,D,E) -> f12(0,B,C,F,G) True (1,1) Signature: {(f0,5);(f12,5);(f25,5);(f36,5)} Flow Graph: [0->{0,3},1->{1,2},2->{},3->{1},4->{0}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E) -> f12(1 + A,B,C,D,E) [A >= 0 && 9 >= A] (?,1) 1. f25(A,B,C,D,E) -> f25(A,1 + B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && 9 >= B] (?,1) 2. f25(A,B,C,D,E) -> f36(A,B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && B >= 10] (?,1) 3. f12(A,B,C,D,E) -> f25(A,0,F,D,E) [A >= 0 && A >= 10] (?,1) 4. f0(A,B,C,D,E) -> f12(0,B,C,F,G) True (1,1) 5. f25(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(exitus616,5);(f0,5);(f12,5);(f25,5);(f36,5)} Flow Graph: [0->{0,3},1->{1,2,5},2->{},3->{1,2,5},4->{0,3},5->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,2),(4,3)] * Step 5: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f12(A,B,C,D,E) -> f12(1 + A,B,C,D,E) [A >= 0 && 9 >= A] (?,1) 1. f25(A,B,C,D,E) -> f25(A,1 + B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && 9 >= B] (?,1) 2. f25(A,B,C,D,E) -> f36(A,B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && B >= 10] (?,1) 3. f12(A,B,C,D,E) -> f25(A,0,F,D,E) [A >= 0 && A >= 10] (?,1) 4. f0(A,B,C,D,E) -> f12(0,B,C,F,G) True (1,1) 5. f25(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(exitus616,5);(f0,5);(f12,5);(f25,5);(f36,5)} Flow Graph: [0->{0,3},1->{1,2,5},2->{},3->{1,5},4->{0},5->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5] | +- p:[0] c: [0] | `- p:[1] c: [1] * Step 6: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. f12(A,B,C,D,E) -> f12(1 + A,B,C,D,E) [A >= 0 && 9 >= A] (?,1) 1. f25(A,B,C,D,E) -> f25(A,1 + B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && 9 >= B] (?,1) 2. f25(A,B,C,D,E) -> f36(A,B,C,D,E) [B >= 0 && -10 + A + B >= 0 && -10 + A >= 0 && B >= 10] (?,1) 3. f12(A,B,C,D,E) -> f25(A,0,F,D,E) [A >= 0 && A >= 10] (?,1) 4. f0(A,B,C,D,E) -> f12(0,B,C,F,G) True (1,1) 5. f25(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(exitus616,5);(f0,5);(f12,5);(f25,5);(f36,5)} Flow Graph: [0->{0,3},1->{1,2,5},2->{},3->{1,5},4->{0},5->{}] ,We construct a looptree: P: [0,1,2,3,4,5] | +- p:[0] c: [0] | `- p:[1] c: [1]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.1] f12 ~> f12 [A <= 10*K, B <= B, C <= C, D <= D, E <= E] f25 ~> f25 [A <= A, B <= 10*K, C <= C, D <= D, E <= E] f25 ~> f36 [A <= A, B <= B, C <= C, D <= D, E <= E] f12 ~> f25 [A <= A, B <= 0*K, C <= unknown, D <= D, E <= E] f0 ~> f12 [A <= 0*K, B <= B, C <= C, D <= unknown, E <= unknown] f25 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= 10*K + A] f12 ~> f12 [A <= 10*K, B <= B, C <= C, D <= D, E <= E] + Loop: [0.1 <= 10*K + B] f25 ~> f25 [A <= A, B <= 10*K, C <= C, D <= D, E <= E] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.1] f12 ~> f12 [K ~=> A] f25 ~> f25 [K ~=> B] f25 ~> f36 [] f12 ~> f25 [K ~=> B,huge ~=> C] f0 ~> f12 [K ~=> A,huge ~=> D,huge ~=> E] f25 ~> exitus616 [] + Loop: [A ~+> 0.0,K ~*> 0.0] f12 ~> f12 [K ~=> A] + Loop: [B ~+> 0.1,K ~*> 0.1] f25 ~> f25 [K ~=> B] + Applied Processor: LareProcessor + Details: f0 ~> f36 [K ~=> A ,K ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] f0 ~> exitus616 [K ~=> A ,K ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] + f12> [K ~=> A,A ~+> 0.0,A ~+> tick,tick ~+> tick,K ~*> 0.0,K ~*> tick] + f25> [K ~=> B,B ~+> 0.1,B ~+> tick,tick ~+> tick,K ~*> 0.1,K ~*> tick] YES(?,O(1))