WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,1,J) [1 >= A && B = C && D = E && F = A && G = H && I = J] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (?,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
6. lbl13(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + G >= 2 && 1 + G >= 0 && A >= 2 + G && F = A && I = A && 1 + D = A] (?,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (?,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[0->{},1->{4,5},2->{2,3},3->{6,7},4->{2,3},5->{6,7},6->{},7->{4,5},8->{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) (<0,0,E>, E, .= 0) (<0,0,F>, F, .= 0) (<0,0,G>, G, .= 0) (<0,0,H>, H, .= 0) (<0,0,I>, 1, .= 1) (<0,0,J>, J, .= 0)
(<1,0,A>, A, .= 0) (<1,0,B>, ?, .?) (<1,0,C>, C, .= 0) (<1,0,D>, D, .= 0) (<1,0,E>, E, .= 0) (<1,0,F>, F, .= 0) (<1,0,G>, G, .= 0) (<1,0,H>, H, .= 0) (<1,0,I>, 1, .= 1) (<1,0,J>, J, .= 0)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0) (<2,0,E>, E, .= 0) (<2,0,F>, F, .= 0) (<2,0,G>, 2 + G, .+ 2) (<2,0,H>, H, .= 0) (<2,0,I>, I, .= 0) (<2,0,J>, J, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0) (<3,0,D>, I, .= 0) (<3,0,E>, E, .= 0) (<3,0,F>, F, .= 0) (<3,0,G>, G, .= 0) (<3,0,H>, H, .= 0) (<3,0,I>, 1 + I, .+ 1) (<3,0,J>, J, .= 0)
(<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>, C, .= 0) (<4,0,D>, D, .= 0) (<4,0,E>, E, .= 0) (<4,0,F>, F, .= 0) (<4,0,G>, 2 + I, .+ 2) (<4,0,H>, H, .= 0) (<4,0,I>, I, .= 0) (<4,0,J>, J, .= 0)
(<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, I, .= 0) (<5,0,E>, E, .= 0) (<5,0,F>, F, .= 0) (<5,0,G>, 1 + I, .+ 1) (<5,0,H>, H, .= 0) (<5,0,I>, 2 + I, .+ 2) (<5,0,J>, J, .= 0)
(<6,0,A>, A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<6,0,D>, D, .= 0) (<6,0,E>, E, .= 0) (<6,0,F>, F, .= 0) (<6,0,G>, G, .= 0) (<6,0,H>, H, .= 0) (<6,0,I>, I, .= 0) (<6,0,J>, J, .= 0)
(<7,0,A>, A, .= 0) (<7,0,B>, ?, .?) (<7,0,C>, C, .= 0) (<7,0,D>, D, .= 0) (<7,0,E>, E, .= 0) (<7,0,F>, F, .= 0) (<7,0,G>, G, .= 0) (<7,0,H>, H, .= 0) (<7,0,I>, I, .= 0) (<7,0,J>, J, .= 0)
(<8,0,A>, A, .= 0) (<8,0,B>, C, .= 0) (<8,0,C>, C, .= 0) (<8,0,D>, E, .= 0) (<8,0,E>, E, .= 0) (<8,0,F>, A, .= 0) (<8,0,G>, H, .= 0) (<8,0,H>, H, .= 0) (<8,0,I>, J, .= 0) (<8,0,J>, J, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,1,J) [1 >= A && B = C && D = E && F = A && G = H && I = J] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (?,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
6. lbl13(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + G >= 2 && 1 + G >= 0 && A >= 2 + G && F = A && I = A && 1 + D = A] (?,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (?,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[0->{},1->{4,5},2->{2,3},3->{6,7},4->{2,3},5->{6,7},6->{},7->{4,5},8->{0,1}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) (<0,0,E>, ?) (<0,0,F>, ?) (<0,0,G>, ?) (<0,0,H>, ?) (<0,0,I>, ?) (<0,0,J>, ?)
(<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<1,0,E>, ?) (<1,0,F>, ?) (<1,0,G>, ?) (<1,0,H>, ?) (<1,0,I>, ?) (<1,0,J>, ?)
(<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) (<2,0,E>, ?) (<2,0,F>, ?) (<2,0,G>, ?) (<2,0,H>, ?) (<2,0,I>, ?) (<2,0,J>, ?)
(<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?) (<3,0,E>, ?) (<3,0,F>, ?) (<3,0,G>, ?) (<3,0,H>, ?) (<3,0,I>, ?) (<3,0,J>, ?)
(<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) (<4,0,E>, ?) (<4,0,F>, ?) (<4,0,G>, ?) (<4,0,H>, ?) (<4,0,I>, ?) (<4,0,J>, ?)
(<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?) (<5,0,E>, ?) (<5,0,F>, ?) (<5,0,G>, ?) (<5,0,H>, ?) (<5,0,I>, ?) (<5,0,J>, ?)
(<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?) (<6,0,E>, ?) (<6,0,F>, ?) (<6,0,G>, ?) (<6,0,H>, ?) (<6,0,I>, ?) (<6,0,J>, ?)
(<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?) (<7,0,E>, ?) (<7,0,F>, ?) (<7,0,G>, ?) (<7,0,H>, ?) (<7,0,I>, ?) (<7,0,J>, ?)
(<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,0,D>, ?) (<8,0,E>, ?) (<8,0,F>, ?) (<8,0,G>, ?) (<8,0,H>, ?) (<8,0,I>, ?) (<8,0,J>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, C) (<0,0,C>, C) (<0,0,D>, E) (<0,0,E>, E) (<0,0,F>, A) (<0,0,G>, H) (<0,0,H>, H) (<0,0,I>, 1) (<0,0,J>, J)
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<6,0,A>, A) (<6,0,B>, ?) (<6,0,C>, C) (<6,0,D>, 1 + A) (<6,0,E>, E) (<6,0,F>, A) (<6,0,G>, 3 + A) (<6,0,H>, H) (<6,0,I>, A) (<6,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
* Step 3: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,1,J) [1 >= A && B = C && D = E && F = A && G = H && I = J] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (?,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
6. lbl13(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + G >= 2 && 1 + G >= 0 && A >= 2 + G && F = A && I = A && 1 + D = A] (?,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (?,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[0->{},1->{4,5},2->{2,3},3->{6,7},4->{2,3},5->{6,7},6->{},7->{4,5},8->{0,1}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, C) (<0,0,C>, C) (<0,0,D>, E) (<0,0,E>, E) (<0,0,F>, A) (<0,0,G>, H) (<0,0,H>, H) (<0,0,I>, 1) (<0,0,J>, J)
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<6,0,A>, A) (<6,0,B>, ?) (<6,0,C>, C) (<6,0,D>, 1 + A) (<6,0,E>, E) (<6,0,F>, A) (<6,0,G>, 3 + A) (<6,0,H>, H) (<6,0,I>, A) (<6,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [0,6]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (?,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (?,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[1->{4,5},2->{2,3},3->{7},4->{2,3},5->{7},7->{4,5},8->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl13) = x1 + -1*x4
p(lbl31) = x1 + -1*x9
p(lbl43) = x1 + -1*x9
p(start) = -1 + x1
p(start0) = -1 + x1
The following rules are strictly oriented:
[A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] ==>
lbl13(A,B,C,D,E,F,G,H,I,J) = A + -1*D
> A + -1*I
= lbl31(A,K,C,D,E,F,G,H,I,J)
The following rules are weakly oriented:
[A >= 2 && B = C && D = E && F = A && G = H && I = J] ==>
start(A,B,C,D,E,F,G,H,I,J) = -1 + A
>= -1 + A
= lbl31(A,K,C,D,E,F,G,H,1,J)
[G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] ==>
lbl43(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl43(A,B,C,D,E,F,-1 + G,H,I,J)
[I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] ==>
lbl43(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl13(A,B,C,I,E,F,G,H,1 + I,J)
[I >= 1 && A >= 1 + I && F = A] ==>
lbl31(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl43(A,B,C,D,E,F,-2 + I,H,I,J)
[I >= 1 && A >= 1 + I && F = A] ==>
lbl31(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J)
True ==>
start0(A,B,C,D,E,F,G,H,I,J) = -1 + A
>= -1 + A
= start(A,C,C,E,E,A,H,H,J,J)
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (?,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (?,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (1 + A,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[1->{4,5},2->{2,3},3->{7},4->{2,3},5->{7},7->{4,5},8->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (1,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (2 + A,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (2 + A,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (1 + A,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[1->{4,5},2->{2,3},3->{7},4->{2,3},5->{7},7->{4,5},8->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl13) = x1 + -1*x9
p(lbl31) = x1 + -1*x9
p(lbl43) = x1 + -1*x9
p(start) = -1 + x1
p(start0) = -1 + x1
The following rules are strictly oriented:
[I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] ==>
lbl43(A,B,C,D,E,F,G,H,I,J) = A + -1*I
> -1 + A + -1*I
= lbl13(A,B,C,I,E,F,G,H,1 + I,J)
[I >= 1 && A >= 1 + I && F = A] ==>
lbl31(A,B,C,D,E,F,G,H,I,J) = A + -1*I
> -1 + A + -1*I
= lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J)
The following rules are weakly oriented:
[A >= 2 && B = C && D = E && F = A && G = H && I = J] ==>
start(A,B,C,D,E,F,G,H,I,J) = -1 + A
>= -1 + A
= lbl31(A,K,C,D,E,F,G,H,1,J)
[G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] ==>
lbl43(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl43(A,B,C,D,E,F,-1 + G,H,I,J)
[I >= 1 && A >= 1 + I && F = A] ==>
lbl31(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl43(A,B,C,D,E,F,-2 + I,H,I,J)
[A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] ==>
lbl13(A,B,C,D,E,F,G,H,I,J) = A + -1*I
>= A + -1*I
= lbl31(A,K,C,D,E,F,G,H,I,J)
True ==>
start0(A,B,C,D,E,F,G,H,I,J) = -1 + A
>= -1 + A
= start(A,C,C,E,E,A,H,H,J,J)
* Step 7: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (1,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (?,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (1 + A,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (2 + A,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (1 + A,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (1 + A,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[1->{4,5},2->{2,3},3->{7},4->{2,3},5->{7},7->{4,5},8->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [4,3,2,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl13) = 1 + x7
p(lbl31) = x9
p(lbl43) = 1 + x7
The following rules are strictly oriented:
[G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] ==>
lbl43(A,B,C,D,E,F,G,H,I,J) = 1 + G
> G
= lbl43(A,B,C,D,E,F,-1 + G,H,I,J)
[I >= 1 && A >= 1 + I && F = A] ==>
lbl31(A,B,C,D,E,F,G,H,I,J) = I
> -1 + I
= lbl43(A,B,C,D,E,F,-2 + I,H,I,J)
The following rules are weakly oriented:
[I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] ==>
lbl43(A,B,C,D,E,F,G,H,I,J) = 1 + G
>= 1 + G
= lbl13(A,B,C,I,E,F,G,H,1 + I,J)
[I >= 1 && A >= 1 + I && F = A] ==>
lbl31(A,B,C,D,E,F,G,H,I,J) = I
>= I
= lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J)
We use the following global sizebounds:
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
* Step 8: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,1,J) [A >= 2 && B = C && D = E && F = A && G = H && I = J] (1,1)
2. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-1 + G,H,I,J) [G >= 0 && I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (1 + A + A^2,1)
3. lbl43(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,G,H,1 + I,J) [I >= 2 + G && 1 + G >= 0 && A >= 1 + I && F = A] (1 + A,1)
4. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl43(A,B,C,D,E,F,-2 + I,H,I,J) [I >= 1 && A >= 1 + I && F = A] (2 + A,1)
5. lbl31(A,B,C,D,E,F,G,H,I,J) -> lbl13(A,B,C,I,E,F,-1 + I,H,1 + I,J) [I >= 1 && A >= 1 + I && F = A] (1 + A,1)
7. lbl13(A,B,C,D,E,F,G,H,I,J) -> lbl31(A,K,C,D,E,F,G,H,I,J) [A >= 2 + D && D + G >= 1 && 1 + G >= 0 && A >= 1 + D && D >= 1 + G && F = A && I = 1 + D] (1 + A,1)
8. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,A,H,H,J,J) True (1,1)
Signature:
{(lbl13,10);(lbl31,10);(lbl43,10);(start,10);(start0,10);(stop,10)}
Flow Graph:
[1->{4,5},2->{2,3},3->{7},4->{2,3},5->{7},7->{4,5},8->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, ?) (<1,0,C>, C) (<1,0,D>, E) (<1,0,E>, E) (<1,0,F>, A) (<1,0,G>, H) (<1,0,H>, H) (<1,0,I>, 1) (<1,0,J>, J)
(<2,0,A>, A) (<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, 1 + A + E) (<2,0,E>, E) (<2,0,F>, A) (<2,0,G>, A) (<2,0,H>, H) (<2,0,I>, A) (<2,0,J>, J)
(<3,0,A>, A) (<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, A) (<3,0,E>, E) (<3,0,F>, A) (<3,0,G>, 3 + A) (<3,0,H>, H) (<3,0,I>, A) (<3,0,J>, J)
(<4,0,A>, A) (<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, 1 + A + E) (<4,0,E>, E) (<4,0,F>, A) (<4,0,G>, 3 + A) (<4,0,H>, H) (<4,0,I>, A) (<4,0,J>, J)
(<5,0,A>, A) (<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, 1 + A) (<5,0,E>, E) (<5,0,F>, A) (<5,0,G>, 2 + A) (<5,0,H>, H) (<5,0,I>, A) (<5,0,J>, J)
(<7,0,A>, A) (<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, 1 + A) (<7,0,E>, E) (<7,0,F>, A) (<7,0,G>, 3 + A) (<7,0,H>, H) (<7,0,I>, A) (<7,0,J>, J)
(<8,0,A>, A) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, E) (<8,0,E>, E) (<8,0,F>, A) (<8,0,G>, H) (<8,0,H>, H) (<8,0,I>, J) (<8,0,J>, J)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))