YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f300(A,B,C,D,E) -> f300(-1 + A,B,C,D,E) [1000 + -1*A >= 0 && A >= 101 && 9 >= B] (?,1) 1. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && 100 >= A && 9 >= B] (?,1) 2. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && B >= 10] (?,1) 3. f1(A,B,C,D,E) -> f300(1000,B,C,D,E) True (1,1) Signature: {(f1,5);(f2,5);(f300,5)} Flow Graph: [0->{0,1,2},1->{},2->{},3->{0,1,2}] + 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. f300(A,B,C,D,E) -> f300(-1 + A,B,C,D,E) [1000 + -1*A >= 0 && A >= 101 && 9 >= B] (?,1) 1. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && 100 >= A && 9 >= B] (1,1) 2. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && B >= 10] (1,1) 3. f1(A,B,C,D,E) -> f300(1000,B,C,D,E) True (1,1) Signature: {(f1,5);(f2,5);(f300,5)} Flow Graph: [0->{0,1,2},1->{},2->{},3->{0,1,2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2),(3,1)] * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f300(A,B,C,D,E) -> f300(-1 + A,B,C,D,E) [1000 + -1*A >= 0 && A >= 101 && 9 >= B] (?,1) 1. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && 100 >= A && 9 >= B] (1,1) 2. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && B >= 10] (1,1) 3. f1(A,B,C,D,E) -> f300(1000,B,C,D,E) True (1,1) Signature: {(f1,5);(f2,5);(f300,5)} Flow Graph: [0->{0,1},1->{},2->{},3->{0,2}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f300(A,B,C,D,E) -> f300(-1 + A,B,C,D,E) [1000 + -1*A >= 0 && A >= 101 && 9 >= B] (?,1) 1. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && 100 >= A && 9 >= B] (?,1) 2. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && B >= 10] (?,1) 3. f1(A,B,C,D,E) -> f300(1000,B,C,D,E) True (1,1) 4. f300(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(exitus616,5);(f1,5);(f2,5);(f300,5)} Flow Graph: [0->{0,1,2,4},1->{},2->{},3->{0,1,2,4},4->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2),(3,1)] * Step 5: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f300(A,B,C,D,E) -> f300(-1 + A,B,C,D,E) [1000 + -1*A >= 0 && A >= 101 && 9 >= B] (?,1) 1. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && 100 >= A && 9 >= B] (?,1) 2. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && B >= 10] (?,1) 3. f1(A,B,C,D,E) -> f300(1000,B,C,D,E) True (1,1) 4. f300(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(exitus616,5);(f1,5);(f2,5);(f300,5)} Flow Graph: [0->{0,1,4},1->{},2->{},3->{0,2,4},4->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4] | `- p:[0] c: [0] * Step 6: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. f300(A,B,C,D,E) -> f300(-1 + A,B,C,D,E) [1000 + -1*A >= 0 && A >= 101 && 9 >= B] (?,1) 1. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && 100 >= A && 9 >= B] (?,1) 2. f300(A,B,C,D,E) -> f2(A,B,0,0,0) [1000 + -1*A >= 0 && B >= 10] (?,1) 3. f1(A,B,C,D,E) -> f300(1000,B,C,D,E) True (1,1) 4. f300(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(exitus616,5);(f1,5);(f2,5);(f300,5)} Flow Graph: [0->{0,1,4},1->{},2->{},3->{0,2,4},4->{}] ,We construct a looptree: P: [0,1,2,3,4] | `- p:[0] c: [0]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0] f300 ~> f300 [A <= 999*K, B <= B, C <= C, D <= D, E <= E] f300 ~> f2 [A <= A, B <= B, C <= 0*K, D <= 0*K, E <= 0*K] f300 ~> f2 [A <= A, B <= B, C <= 0*K, D <= 0*K, E <= 0*K] f1 ~> f300 [A <= 1000*K, B <= B, C <= C, D <= D, E <= E] f300 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= A] f300 ~> f300 [A <= 999*K, B <= B, 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] f300 ~> f300 [K ~=> A] f300 ~> f2 [K ~=> C,K ~=> D,K ~=> E] f300 ~> f2 [K ~=> C,K ~=> D,K ~=> E] f1 ~> f300 [K ~=> A] f300 ~> exitus616 [] + Loop: [A ~=> 0.0] f300 ~> f300 [K ~=> A] + Applied Processor: LareProcessor + Details: f1 ~> exitus616 [K ~=> A,K ~=> 0.0,tick ~+> tick,K ~+> tick] f1 ~> f2 [K ~=> A,K ~=> C,K ~=> D,K ~=> E,K ~=> 0.0,tick ~+> tick,K ~+> tick] + f300> [A ~=> 0.0,K ~=> A,A ~+> tick,tick ~+> tick] YES(?,O(1))