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