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