YES(?,O(1)) * Step 1: ArgumentFilter WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E) -> f7(F,0,0,D,E) [0 >= 1 + F] (1,1) 1. f0(A,B,C,D,E) -> f7(F,0,0,D,E) [F >= 1] (1,1) 2. f0(A,B,C,D,E) -> f7(0,1023,0,D,E) True (1,1) 3. f7(A,B,C,D,E) -> f7(A,B,1 + C,2 + D,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && B >= C] (?,1) 4. f7(A,B,C,D,E) -> f21(A,B,C,D,E) [C >= 0 (?,1) && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && E >= 0 && C >= 1 + B && 1022 >= E] 5. f7(A,B,C,D,E) -> f21(A,B,C,D,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && E >= 1023] (?,1) 6. f7(A,B,C,D,E) -> f21(A,B,C,D,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && 0 >= 1 + E] (?,1) Signature: {(f0,5);(f21,5);(f7,5)} Flow Graph: [0->{3,4,5,6},1->{3,4,5,6},2->{3,4,5,6},3->{3,4,5,6},4->{},5->{},6->{}] + Applied Processor: ArgumentFilter [0,3] + Details: We remove following argument positions: [0,3]. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1) 1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1) 2. f0(B,C,E) -> f7(1023,0,E) True (1,1) 3. f7(B,C,E) -> f7(B,1 + C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && B >= C] (?,1) 4. f7(B,C,E) -> f21(B,C,E) [C >= 0 (?,1) && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && E >= 0 && C >= 1 + B && 1022 >= E] 5. f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && E >= 1023] (?,1) 6. f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && 0 >= 1 + E] (?,1) Signature: {(f0,5);(f21,5);(f7,5)} Flow Graph: [0->{3,4,5,6},1->{3,4,5,6},2->{3,4,5,6},3->{3,4,5,6},4->{},5->{},6->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,4),(0,5),(0,6),(1,4),(1,5),(1,6),(2,4),(2,5),(2,6)] * Step 3: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1) 1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1) 2. f0(B,C,E) -> f7(1023,0,E) True (1,1) 3. f7(B,C,E) -> f7(B,1 + C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && B >= C] (?,1) 4. f7(B,C,E) -> f21(B,C,E) [C >= 0 (?,1) && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && E >= 0 && C >= 1 + B && 1022 >= E] 5. f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && E >= 1023] (?,1) 6. f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && 0 >= 1 + E] (?,1) Signature: {(f0,5);(f21,5);(f7,5)} Flow Graph: [0->{3},1->{3},2->{3},3->{3,4,5,6},4->{},5->{},6->{}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] f0(B,C,E) -> f7(0,0,E) [F >= 1] f0(B,C,E) -> f7(1023,0,E) True f7(B,C,E) -> f7(B,1 + C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && B >= C] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && E >= 0 && C >= 1 + B && 1022 >= E] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && E >= 1023] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && 0 >= 1 + E] Signature: {(f0,5);(f21,5);(f7,5)} Rule Graph: [0->{3},1->{3},2->{3},3->{3,4,5,6},4->{},5->{},6->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] f0(B,C,E) -> f7(0,0,E) [F >= 1] f0(B,C,E) -> f7(1023,0,E) True f7(B,C,E) -> f7(B,1 + C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && B >= C] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && E >= 0 && C >= 1 + B && 1022 >= E] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && E >= 1023] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && 0 >= 1 + E] f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True Signature: {(exitus616,3);(f0,5);(f21,5);(f7,5)} Rule Graph: [0->{3},1->{3},2->{3},3->{3,4,5,6},4->{9,12,15},5->{8,11,14},6->{7,10,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,14,15] | `- p:[3] c: [3] * Step 6: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] f0(B,C,E) -> f7(0,0,E) [F >= 1] f0(B,C,E) -> f7(1023,0,E) True f7(B,C,E) -> f7(B,1 + C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && B >= C] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && E >= 0 && C >= 1 + B && 1022 >= E] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && E >= 1023] f7(B,C,E) -> f21(B,C,E) [C >= 0 && B + C >= 0 && 1023 + -1*B + C >= 0 && 1023 + -1*B >= 0 && B >= 0 && C >= 1 + B && 0 >= 1 + E] f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True f21(B,C,E) -> exitus616(B,C,E) True Signature: {(exitus616,3);(f0,5);(f21,5);(f7,5)} Rule Graph: [0->{3},1->{3},2->{3},3->{3,4,5,6},4->{9,12,15},5->{8,11,14},6->{7,10,13}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15] | `- p:[3] c: [3]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [B,C,E,0.0] f0 ~> f7 [B <= 0*K, C <= 0*K, E <= E] f0 ~> f7 [B <= 0*K, C <= 0*K, E <= E] f0 ~> f7 [B <= 1023*K, C <= 0*K, E <= E] f7 ~> f7 [B <= B, C <= 1024*K, E <= E] f7 ~> f21 [B <= B, C <= C, E <= E] f7 ~> f21 [B <= B, C <= C, E <= E] f7 ~> f21 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] f21 ~> exitus616 [B <= B, C <= C, E <= E] + Loop: [0.0 <= B + C] f7 ~> f7 [B <= B, C <= 1024*K, E <= E] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,B,C,E,0.0] f0 ~> f7 [K ~=> B,K ~=> C] f0 ~> f7 [K ~=> B,K ~=> C] f0 ~> f7 [K ~=> B,K ~=> C] f7 ~> f7 [K ~=> C] f7 ~> f21 [] f7 ~> f21 [] f7 ~> f21 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] f21 ~> exitus616 [] + Loop: [B ~+> 0.0,C ~+> 0.0] f7 ~> f7 [K ~=> C] + Applied Processor: Lare + Details: f0 ~> exitus616 [K ~=> B,K ~=> C,tick ~+> tick,K ~+> 0.0,K ~+> tick,K ~*> 0.0,K ~*> tick] + f7> [K ~=> C,B ~+> 0.0,B ~+> tick,C ~+> 0.0,C ~+> tick,tick ~+> tick] YES(?,O(1))