WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop1(A,B,C,D) [A >= 0 && B >= 0 && C >= 0 && D = 0] (?,1) 1. start(A,B,C,D) -> cont1(A,B,C,D) [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1) 2. cont1(A,B,C,D) -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0] (?,1) 3. cont1(A,B,C,D) -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] (?,1) 4. a(A,B,C,D) -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1] (?,1) 5. b(A,B,C,D) -> start(A,B,C,D) [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 6. b(A,B,C,D) -> stop3(A,B,C,D) [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 7. start0(A,B,C,D) -> start(A,B,B,A) [A >= 0 && B >= 0] (1,1) Signature: {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)} Flow Graph: [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,A>, A, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>, C, .= 0) (<0,0,D>, D, .= 0) (<1,0,A>, A, .= 0) (<1,0,B>, B, .= 0) (<1,0,C>, C, .= 0) (<1,0,D>, D, .= 0) (<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, 1, .= 1) (<2,0,D>, 1 + D, .+ 1) (<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, 1 + C, .+ 1) (<3,0,D>, D, .= 0) (<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>, ?, .?) (<4,0,D>, 1 + A + D, .* 1) (<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, D, .= 0) (<6,0,A>, A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<6,0,D>, D, .= 0) (<7,0,A>, A, .= 0) (<7,0,B>, B, .= 0) (<7,0,C>, B, .= 0) (<7,0,D>, A, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop1(A,B,C,D) [A >= 0 && B >= 0 && C >= 0 && D = 0] (?,1) 1. start(A,B,C,D) -> cont1(A,B,C,D) [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1) 2. cont1(A,B,C,D) -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0] (?,1) 3. cont1(A,B,C,D) -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] (?,1) 4. a(A,B,C,D) -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1] (?,1) 5. b(A,B,C,D) -> start(A,B,C,D) [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 6. b(A,B,C,D) -> stop3(A,B,C,D) [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 7. start0(A,B,C,D) -> start(A,B,B,A) [A >= 0 && B >= 0] (1,1) Signature: {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)} Flow Graph: [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) (<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?) (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?) (<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?) (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, ?) (<0,0,D>, A) (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) (<2,0,A>, A) (<2,0,B>, B) (<2,0,C>, 1) (<2,0,D>, 1 + A) (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) (<6,0,A>, A) (<6,0,B>, B) (<6,0,C>, ?) (<6,0,D>, A) (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) * Step 3: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop1(A,B,C,D) [A >= 0 && B >= 0 && C >= 0 && D = 0] (?,1) 1. start(A,B,C,D) -> cont1(A,B,C,D) [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1) 2. cont1(A,B,C,D) -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0] (?,1) 3. cont1(A,B,C,D) -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] (?,1) 4. a(A,B,C,D) -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1] (?,1) 5. b(A,B,C,D) -> start(A,B,C,D) [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 6. b(A,B,C,D) -> stop3(A,B,C,D) [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 7. start0(A,B,C,D) -> start(A,B,B,A) [A >= 0 && B >= 0] (1,1) Signature: {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)} Flow Graph: [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, ?) (<0,0,D>, A) (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) (<2,0,A>, A) (<2,0,B>, B) (<2,0,C>, 1) (<2,0,D>, 1 + A) (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) (<6,0,A>, A) (<6,0,B>, B) (<6,0,C>, ?) (<6,0,D>, A) (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [0,2,6] * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D) -> cont1(A,B,C,D) [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1) 3. cont1(A,B,C,D) -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] (?,1) 4. a(A,B,C,D) -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1] (?,1) 5. b(A,B,C,D) -> start(A,B,C,D) [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] (?,1) 7. start0(A,B,C,D) -> start(A,B,B,A) [A >= 0 && B >= 0] (1,1) Signature: {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)} Flow Graph: [1->{3},3->{4},4->{5},5->{1},7->{1}] Sizebounds: (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(a) = x4 p(b) = 1 + x4 p(cont1) = x4 p(start) = x4 p(start0) = x1 The following rules are strictly oriented: [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] ==> b(A,B,C,D) = 1 + D > D = start(A,B,C,D) The following rules are weakly oriented: [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] ==> start(A,B,C,D) = D >= D = cont1(A,B,C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] ==> cont1(A,B,C,D) = D >= D = a(A,B,-1 + C,D) [A >= D && B >= 0 && C >= 0 && D >= 1] ==> a(A,B,C,D) = D >= D = b(A,B,E,-1 + D) [A >= 0 && B >= 0] ==> start0(A,B,C,D) = A >= A = start(A,B,B,A) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D) -> cont1(A,B,C,D) [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1) 3. cont1(A,B,C,D) -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] (?,1) 4. a(A,B,C,D) -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1] (?,1) 5. b(A,B,C,D) -> start(A,B,C,D) [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] (A,1) 7. start0(A,B,C,D) -> start(A,B,B,A) [A >= 0 && B >= 0] (1,1) Signature: {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)} Flow Graph: [1->{3},3->{4},4->{5},5->{1},7->{1}] Sizebounds: (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D) -> cont1(A,B,C,D) [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (1 + A,1) 3. cont1(A,B,C,D) -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] (1 + A,1) 4. a(A,B,C,D) -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1] (1 + A,1) 5. b(A,B,C,D) -> start(A,B,C,D) [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] (A,1) 7. start0(A,B,C,D) -> start(A,B,B,A) [A >= 0 && B >= 0] (1,1) Signature: {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)} Flow Graph: [1->{3},3->{4},4->{5},5->{1},7->{1}] Sizebounds: (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^1))