WORST_CASE(?,O(n^1))
* Step 1: UnsatRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
2. lbl161(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [89 >= A && D = 1 && H = A && F = 101 && B = 91] (?,1)
3. lbl161(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [0 >= 10 && 89 >= A && 0 >= 1 && D = 2 && H = A && F = 101 && B = 91] (?,1)
4. lbl161(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [0 >= 2 && 89 >= A && H = A && F = 101 && D = 1 && B = 91] (?,1)
5. lbl161(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [0 >= 1 && 89 >= A && H = A && F = 101 && D = 1 && B = 91] (?,1)
6. lbl161(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [0 >= 10 && 0 >= 2 && 89 >= A && H = A && F = 101 && D = 1 && B = 91] (?,1)
7. lbl221(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [1 >= D && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
8. lbl221(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A && 89 >= A && F = 111 && D = 2 && H = A && B = C] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
13. lbl111(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A + 11*D >= 112 && 1 >= D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
14. lbl111(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 && D = 2 && H = 100 && B = C && A = 100] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,13,14,15,16,17},2->{},3->{2,3,4,5,6},4->{7,8,9,10,11},5->{7,8,9,10,11},6->{7,8,9,10,11}
,7->{},8->{2,3,4,5,6},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{7,8,9,10,11},12->{12,13,14,15,16,17},13->{}
,14->{2,3,4,5,6},15->{7,8,9,10,11},16->{7,8,9,10,11},17->{7,8,9,10,11},18->{0,1}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [3,4,5,6,7,13]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
2. lbl161(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [89 >= A && D = 1 && H = A && F = 101 && B = 91] (?,1)
8. lbl221(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A && 89 >= A && F = 111 && D = 2 && H = A && B = C] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
14. lbl111(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 && D = 2 && H = 100 && B = C && A = 100] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,14,15,16,17},2->{},8->{2},9->{8,9,10,11},10->{8,9,10,11},11->{8,9,10,11},12->{12,14,15,16
,17},14->{2},15->{8,9,10,11},16->{8,9,10,11},17->{8,9,10,11},18->{0,1}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, 10 + H, .+ 10) (< 0,0,C>, C, .= 0) (< 0,0,D>, 1, .= 1) (< 0,0,E>, E, .= 0) (< 0,0,F>, H, .= 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>, 2, .= 2) (< 1,0,E>, E, .= 0) (< 1,0,F>, 11 + H, .+ 11) (< 1,0,G>, G, .= 0) (< 1,0,H>, H, .= 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>, G, .= 0) (< 2,0,H>, H, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, 91, .= 91) (< 8,0,C>, C, .= 0) (< 8,0,D>, 1, .= 1) (< 8,0,E>, E, .= 0) (< 8,0,F>, 101, .= 101) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, 111, .= 111) (< 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>, E, .= 0) (<10,0,F>, 111, .= 111) (<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>, 1 + D, .+ 1) (<11,0,E>, E, .= 0) (<11,0,F>, 102, .= 102) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, 1 + D, .+ 1) (<12,0,E>, E, .= 0) (<12,0,F>, 11 + F, .+ 11) (<12,0,G>, G, .= 0) (<12,0,H>, H, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, 91, .= 91) (<14,0,C>, C, .= 0) (<14,0,D>, 1, .= 1) (<14,0,E>, E, .= 0) (<14,0,F>, 101, .= 101) (<14,0,G>, G, .= 0) (<14,0,H>, H, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0) (<15,0,E>, E, .= 0) (<15,0,F>, 111, .= 111) (<15,0,G>, G, .= 0) (<15,0,H>, H, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0) (<16,0,E>, E, .= 0) (<16,0,F>, 111, .= 111) (<16,0,G>, G, .= 0) (<16,0,H>, H, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, C, .= 0) (<17,0,D>, 2 + D, .+ 2) (<17,0,E>, E, .= 0) (<17,0,F>, 102, .= 102) (<17,0,G>, G, .= 0) (<17,0,H>, H, .= 0)
(<18,0,A>, A, .= 0) (<18,0,B>, C, .= 0) (<18,0,C>, C, .= 0) (<18,0,D>, E, .= 0) (<18,0,E>, E, .= 0) (<18,0,F>, G, .= 0) (<18,0,G>, G, .= 0) (<18,0,H>, A, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
2. lbl161(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [89 >= A && D = 1 && H = A && F = 101 && B = 91] (?,1)
8. lbl221(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A && 89 >= A && F = 111 && D = 2 && H = A && B = C] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
14. lbl111(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 && D = 2 && H = 100 && B = C && A = 100] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,14,15,16,17},2->{},8->{2},9->{8,9,10,11},10->{8,9,10,11},11->{8,9,10,11},12->{12,14,15,16
,17},14->{2},15->{8,9,10,11},16->{8,9,10,11},17->{8,9,10,11},18->{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>, ?)
(< 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>, ?)
(< 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>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<15,0,F>, ?) (<15,0,G>, ?) (<15,0,H>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, ?) (<16,0,F>, ?) (<16,0,G>, ?) (<16,0,H>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,E>, ?) (<17,0,F>, ?) (<17,0,G>, ?) (<17,0,H>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,E>, ?) (<18,0,F>, ?) (<18,0,G>, ?) (<18,0,H>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, 10 + A) (< 0,0,C>, C) (< 0,0,D>, 1) (< 0,0,E>, E) (< 0,0,F>, A) (< 0,0,G>, G) (< 0,0,H>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 2) (< 1,0,E>, E) (< 1,0,F>, 11 + A) (< 1,0,G>, G) (< 1,0,H>, A)
(< 2,0,A>, A) (< 2,0,B>, 91) (< 2,0,C>, C) (< 2,0,D>, 1) (< 2,0,E>, E) (< 2,0,F>, 101) (< 2,0,G>, G) (< 2,0,H>, A)
(< 8,0,A>, A) (< 8,0,B>, 91) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, 101) (< 8,0,G>, G) (< 8,0,H>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<14,0,A>, A) (<14,0,B>, 91) (<14,0,C>, C) (<14,0,D>, 1) (<14,0,E>, E) (<14,0,F>, 101) (<14,0,G>, G) (<14,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, A)
* Step 4: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
2. lbl161(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [89 >= A && D = 1 && H = A && F = 101 && B = 91] (?,1)
8. lbl221(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A && 89 >= A && F = 111 && D = 2 && H = A && B = C] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
14. lbl111(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 && D = 2 && H = 100 && B = C && A = 100] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,14,15,16,17},2->{},8->{2},9->{8,9,10,11},10->{8,9,10,11},11->{8,9,10,11},12->{12,14,15,16
,17},14->{2},15->{8,9,10,11},16->{8,9,10,11},17->{8,9,10,11},18->{0,1}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, 10 + A) (< 0,0,C>, C) (< 0,0,D>, 1) (< 0,0,E>, E) (< 0,0,F>, A) (< 0,0,G>, G) (< 0,0,H>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 2) (< 1,0,E>, E) (< 1,0,F>, 11 + A) (< 1,0,G>, G) (< 1,0,H>, A)
(< 2,0,A>, A) (< 2,0,B>, 91) (< 2,0,C>, C) (< 2,0,D>, 1) (< 2,0,E>, E) (< 2,0,F>, 101) (< 2,0,G>, G) (< 2,0,H>, A)
(< 8,0,A>, A) (< 8,0,B>, 91) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, 101) (< 8,0,G>, G) (< 8,0,H>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<14,0,A>, A) (<14,0,B>, 91) (<14,0,C>, C) (<14,0,D>, 1) (<14,0,E>, E) (<14,0,F>, 101) (<14,0,G>, G) (<14,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, A)
+ Applied Processor:
ChainProcessor False [0,1,2,8,9,10,11,12,14,15,16,17,18]
+ Details:
We chained rule 8 to obtain the rules [19] .
* Step 5: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
2. lbl161(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [89 >= A && D = 1 && H = A && F = 101 && B = 91] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
14. lbl111(A,B,C,D,E,F,G,H) -> lbl161(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 && D = 2 && H = 100 && B = C && A = 100] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,14,15,16,17},2->{},9->{9,10,11,19},10->{9,10,11,19},11->{9,10,11,19},12->{12,14,15,16,17}
,14->{2},15->{9,10,11,19},16->{9,10,11,19},17->{9,10,11,19},18->{0,1},19->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, 10 + A) (< 0,0,C>, C) (< 0,0,D>, 1) (< 0,0,E>, E) (< 0,0,F>, A) (< 0,0,G>, G) (< 0,0,H>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 2) (< 1,0,E>, E) (< 1,0,F>, 11 + A) (< 1,0,G>, G) (< 1,0,H>, A)
(< 2,0,A>, A) (< 2,0,B>, 91) (< 2,0,C>, C) (< 2,0,D>, 1) (< 2,0,E>, E) (< 2,0,F>, 101) (< 2,0,G>, G) (< 2,0,H>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<14,0,A>, A) (<14,0,B>, 91) (<14,0,C>, C) (<14,0,D>, 1) (<14,0,E>, E) (<14,0,F>, 101) (<14,0,G>, G) (<14,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
+ Applied Processor:
ChainProcessor False [0,1,2,9,10,11,12,14,15,16,17,18,19]
+ Details:
We chained rule 14 to obtain the rules [20] .
* Step 6: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
2. lbl161(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [89 >= A && D = 1 && H = A && F = 101 && B = 91] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
20. lbl111(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 (?,2)
&& D = 2
&& H = 100
&& B = C
&& A = 100
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,15,16,17,20},2->{},9->{9,10,11,19},10->{9,10,11,19},11->{9,10,11,19},12->{12,15,16,17,20}
,15->{9,10,11,19},16->{9,10,11,19},17->{9,10,11,19},18->{0,1},19->{},20->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, 10 + A) (< 0,0,C>, C) (< 0,0,D>, 1) (< 0,0,E>, E) (< 0,0,F>, A) (< 0,0,G>, G) (< 0,0,H>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 2) (< 1,0,E>, E) (< 1,0,F>, 11 + A) (< 1,0,G>, G) (< 1,0,H>, A)
(< 2,0,A>, A) (< 2,0,B>, 91) (< 2,0,C>, C) (< 2,0,D>, 1) (< 2,0,E>, E) (< 2,0,F>, 101) (< 2,0,G>, G) (< 2,0,H>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
(<20,0,A>, A) (<20,0,B>, 91) (<20,0,C>, C) (<20,0,D>, 1) (<20,0,E>, E) (<20,0,F>, 101) (<20,0,G>, G) (<20,0,H>, A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [2]
* Step 7: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
18. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A) True (1,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
20. lbl111(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 (?,2)
&& D = 2
&& H = 100
&& B = C
&& A = 100
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,15,16,17,20},9->{9,10,11,19},10->{9,10,11,19},11->{9,10,11,19},12->{12,15,16,17,20},15->{9
,10,11,19},16->{9,10,11,19},17->{9,10,11,19},18->{0,1},19->{},20->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, 10 + A) (< 0,0,C>, C) (< 0,0,D>, 1) (< 0,0,E>, E) (< 0,0,F>, A) (< 0,0,G>, G) (< 0,0,H>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 2) (< 1,0,E>, E) (< 1,0,F>, 11 + A) (< 1,0,G>, G) (< 1,0,H>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
(<20,0,A>, A) (<20,0,B>, 91) (<20,0,C>, C) (<20,0,D>, 1) (<20,0,E>, E) (<20,0,F>, 101) (<20,0,G>, G) (<20,0,H>, A)
+ Applied Processor:
ChainProcessor False [0,1,9,10,11,12,15,16,17,18,19,20]
+ Details:
We chained rule 18 to obtain the rules [21,22] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H) -> stop(A,-10 + H,C,1,E,H,G,H) [A >= 101 && B = C && D = E && F = G && H = A] (?,1)
1. start(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,2,E,11 + H,G,H) [100 >= A && B = C && D = E && F = G && H = A] (?,1)
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
20. lbl111(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 (?,2)
&& D = 2
&& H = 100
&& B = C
&& A = 100
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[0->{},1->{12,15,16,17,20},9->{9,10,11,19},10->{9,10,11,19},11->{9,10,11,19},12->{12,15,16,17,20},15->{9
,10,11,19},16->{9,10,11,19},17->{9,10,11,19},19->{},20->{},21->{},22->{12,15,16,17,20}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, 10 + A) (< 0,0,C>, C) (< 0,0,D>, 1) (< 0,0,E>, E) (< 0,0,F>, A) (< 0,0,G>, G) (< 0,0,H>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 2) (< 1,0,E>, E) (< 1,0,F>, 11 + A) (< 1,0,G>, G) (< 1,0,H>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
(<20,0,A>, A) (<20,0,B>, 91) (<20,0,C>, C) (<20,0,D>, 1) (<20,0,E>, E) (<20,0,F>, 101) (<20,0,G>, G) (<20,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [0,1]
* Step 9: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
20. lbl111(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 (?,2)
&& D = 2
&& H = 100
&& B = C
&& A = 100
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11,19},10->{9,10,11,19},11->{9,10,11,19},12->{12,15,16,17,20},15->{9,10,11,19},16->{9,10,11,19}
,17->{9,10,11,19},19->{},20->{},21->{},22->{12,15,16,17,20}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
(<20,0,A>, A) (<20,0,B>, 91) (<20,0,C>, C) (<20,0,D>, 1) (<20,0,E>, E) (<20,0,F>, 101) (<20,0,G>, G) (<20,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(9,19)
,(11,11)
,(11,19)
,(12,20)
,(15,19)
,(16,19)
,(17,11)
,(17,19)
,(22,15)
,(22,17)
,(22,20)]
* Step 10: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
20. lbl111(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [F = 111 (?,2)
&& D = 2
&& H = 100
&& B = C
&& A = 100
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11,19},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},19->{}
,20->{},21->{},22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
(<20,0,A>, A) (<20,0,B>, 91) (<20,0,C>, C) (<20,0,D>, 1) (<20,0,E>, E) (<20,0,F>, 101) (<20,0,G>, G) (<20,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [20]
* Step 11: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
19. lbl221(A,B,C,D,E,F,G,H) -> stop(A,-20 + F,C,-1 + D,E,-10 + F,G,H) [99 >= A (?,2)
&& 89 >= A
&& F = 111
&& D = 2
&& H = A
&& B = C
&& 89 >= A
&& -1 + D = 1
&& H = A
&& -10 + F = 101
&& -20 + F = 91]
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11,19},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},19->{}
,21->{},22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<19,0,A>, A) (<19,0,B>, 91) (<19,0,C>, C) (<19,0,D>, 1) (<19,0,E>, E) (<19,0,F>, 101) (<19,0,G>, G) (<19,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [19]
* Step 12: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, 111, .= 111) (< 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>, E, .= 0) (<10,0,F>, 111, .= 111) (<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>, 1 + D, .+ 1) (<11,0,E>, E, .= 0) (<11,0,F>, 102, .= 102) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, 1 + D, .+ 1) (<12,0,E>, E, .= 0) (<12,0,F>, 11 + F, .+ 11) (<12,0,G>, G, .= 0) (<12,0,H>, H, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0) (<15,0,E>, E, .= 0) (<15,0,F>, 111, .= 111) (<15,0,G>, G, .= 0) (<15,0,H>, H, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0) (<16,0,E>, E, .= 0) (<16,0,F>, 111, .= 111) (<16,0,G>, G, .= 0) (<16,0,H>, H, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, C, .= 0) (<17,0,D>, 2 + D, .+ 2) (<17,0,E>, E, .= 0) (<17,0,F>, 102, .= 102) (<17,0,G>, G, .= 0) (<17,0,H>, H, .= 0)
(<21,0,A>, A, .= 0) (<21,0,B>, 10 + A, .+ 10) (<21,0,C>, C, .= 0) (<21,0,D>, 1, .= 1) (<21,0,E>, E, .= 0) (<21,0,F>, A, .= 0) (<21,0,G>, G, .= 0) (<21,0,H>, A, .= 0)
(<22,0,A>, A, .= 0) (<22,0,B>, C, .= 0) (<22,0,C>, C, .= 0) (<22,0,D>, 2, .= 2) (<22,0,E>, E, .= 0) (<22,0,F>, 11 + A, .+ 11) (<22,0,G>, G, .= 0) (<22,0,H>, A, .= 0)
* Step 13: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 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>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<15,0,F>, ?) (<15,0,G>, ?) (<15,0,H>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, ?) (<16,0,F>, ?) (<16,0,G>, ?) (<16,0,H>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,E>, ?) (<17,0,F>, ?) (<17,0,G>, ?) (<17,0,H>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,0,E>, ?) (<21,0,F>, ?) (<21,0,G>, ?) (<21,0,H>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, ?) (<22,0,F>, ?) (<22,0,G>, ?) (<22,0,H>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
* Step 14: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 9 : [100 >= A] 10 : [100 >= A] 11 : [100 >= A] 12 : [100 >= A
&& 100 >= A] 15 : [False] 16 : [100 >= A] 17 : [False] 21 : True 22 : True .
* Step 15: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (?,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(lbl111) = 1
p(lbl221) = 0
p(start0) = 1
p(stop) = 1
The following rules are strictly oriented:
[D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] ==>
lbl111(A,B,C,D,E,F,G,H) = 1
> 0
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
The following rules are weakly oriented:
[D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] ==>
lbl111(A,B,C,D,E,F,G,H) = 1
>= 1
= lbl111(A,B,C,1 + D,E,11 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 1
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 1
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[A >= 101 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 1
>= 1
= stop(A,-10 + A,C,1,E,A,G,A)
[100 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 1
>= 1
= lbl111(A,C,C,2,E,11 + A,G,A)
* Step 16: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(lbl111) = 1
p(lbl221) = 0
p(start0) = 1
p(stop) = 1
The following rules are strictly oriented:
[A + 11*D >= 112 ==>
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 1
> 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] ==>
lbl111(A,B,C,D,E,F,G,H) = 1
> 0
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
The following rules are weakly oriented:
[D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] ==>
lbl111(A,B,C,D,E,F,G,H) = 1
>= 1
= lbl111(A,B,C,1 + D,E,11 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 1
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[A >= 101 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 1
>= 1
= stop(A,-10 + A,C,1,E,A,G,A)
[100 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 1
>= 1
= lbl111(A,C,C,2,E,11 + A,G,A)
* Step 17: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (?,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(lbl111) = 1
p(lbl221) = 0
p(start0) = 1
p(stop) = 1
The following rules are strictly oriented:
[A + 11*D >= 112 ==>
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 1
> 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 1
> 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] ==>
lbl111(A,B,C,D,E,F,G,H) = 1
> 0
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
The following rules are weakly oriented:
[D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 0
>= 0
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] ==>
lbl111(A,B,C,D,E,F,G,H) = 1
>= 1
= lbl111(A,B,C,1 + D,E,11 + F,G,H)
[A >= 101 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 1
>= 1
= stop(A,-10 + A,C,1,E,A,G,A)
[100 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 1
>= 1
= lbl111(A,C,C,2,E,11 + A,G,A)
* Step 18: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (?,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (?,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = 815 + -8*x1 + -11*x4
p(lbl221) = 658 + 77*x4 + -8*x6
p(start0) = 793 + -8*x1
p(stop) = 793*x4 + -8*x8
The following rules are strictly oriented:
[D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 658 + 77*D + -8*F
> 653 + 77*D + -8*F
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] ==>
lbl111(A,B,C,D,E,F,G,H) = 815 + -8*A + -11*D
> 804 + -8*A + -11*D
= lbl111(A,B,C,1 + D,E,11 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 815 + -8*A + -11*D
> 650 + 77*D + -8*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 815 + -8*A + -11*D
> 650 + 77*D + -8*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] ==>
lbl111(A,B,C,D,E,F,G,H) = 815 + -8*A + -11*D
> 653 + 77*D + -8*F
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
The following rules are weakly oriented:
[D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 658 + 77*D + -8*F
>= 650 + 77*D + -8*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 658 + 77*D + -8*F
>= 650 + 77*D + -8*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[A >= 101 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 793 + -8*A
>= 793 + -8*A
= stop(A,-10 + A,C,1,E,A,G,A)
[100 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 793 + -8*A
>= 793 + -8*A
= lbl111(A,C,C,2,E,11 + A,G,A)
* Step 19: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (793 + 8*A,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (793 + 8*A,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = 606 + -5*x1 + -1*x6
p(lbl221) = 287 + -5*x1 + 11*x4 + -1*x6 + 3*x8
p(start0) = 595 + -6*x1
p(stop) = 595*x4 + -6*x8
The following rules are strictly oriented:
[D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 287 + -5*A + 11*D + -1*F + 3*H
> 286 + -5*A + 11*D + -1*F + 3*H
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 287 + -5*A + 11*D + -1*F + 3*H
> 285 + -5*A + 11*D + -1*F + 3*H
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] ==>
lbl111(A,B,C,D,E,F,G,H) = 606 + -5*A + -1*F
> 595 + -5*A + -1*F
= lbl111(A,B,C,1 + D,E,11 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 606 + -5*A + -1*F
> 286 + -5*A + 11*D + -1*F + 3*H
= lbl221(A,B,C,D,E,1 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 606 + -5*A + -1*F
> 286 + -5*A + 11*D + -1*F + 3*H
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] ==>
lbl111(A,B,C,D,E,F,G,H) = 606 + -5*A + -1*F
> 285 + -5*A + 11*D + -1*F + 3*H
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
The following rules are weakly oriented:
[D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 287 + -5*A + 11*D + -1*F + 3*H
>= 286 + -5*A + 11*D + -1*F + 3*H
= lbl221(A,B,C,D,E,1 + F,G,H)
[A >= 101 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 595 + -6*A
>= 595 + -6*A
= stop(A,-10 + A,C,1,E,A,G,A)
[100 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 595 + -6*A
>= 595 + -6*A
= lbl111(A,C,C,2,E,11 + A,G,A)
* Step 20: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (?,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (595 + 6*A,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (595 + 6*A,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (595 + 6*A,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = 211 + -1*x1 + -1*x6
p(lbl221) = 89 + 11*x4 + -1*x6
p(start0) = 200 + -2*x1
p(stop) = 200*x4 + -2*x8
The following rules are strictly oriented:
[D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 89 + 11*D + -1*F
> 88 + 11*D + -1*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 89 + 11*D + -1*F
> 88 + 11*D + -1*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] ==>
lbl111(A,B,C,D,E,F,G,H) = 211 + -1*A + -1*F
> 200 + -1*A + -1*F
= lbl111(A,B,C,1 + D,E,11 + F,G,H)
The following rules are weakly oriented:
[D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] ==>
lbl221(A,B,C,D,E,F,G,H) = 89 + 11*D + -1*F
>= 87 + 11*D + -1*F
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 211 + -1*A + -1*F
>= 88 + 11*D + -1*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[A + 11*D >= 112 ==>
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
lbl111(A,B,C,D,E,F,G,H) = 211 + -1*A + -1*F
>= 88 + 11*D + -1*F
= lbl221(A,B,C,D,E,1 + F,G,H)
[D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] ==>
lbl111(A,B,C,D,E,F,G,H) = 211 + -1*A + -1*F
>= 87 + 11*D + -1*F
= lbl221(A,B,C,-1 + D,E,-9 + F,G,H)
[A >= 101 && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 200 + -2*A
>= 200 + -2*A
= stop(A,-10 + A,C,1,E,A,G,A)
[100 >= A && C = C && E = E && G = G && A = A] ==>
start0(A,B,C,D,E,F,G,H) = 200 + -2*A
>= 200 + -2*A
= lbl111(A,C,C,2,E,11 + A,G,A)
* Step 21: CombineProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 3 && 110 >= F && D >= 2 && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (200 + 2*A,1)
10. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [D >= 2 && 110 >= F && F >= 102 && 111 >= F && 10 + F >= A + 11*D && 89 >= A && H = A && B = C] (200 + 2*A,1)
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (595 + 6*A,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (200 + 2*A,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[9->{9,10,11},10->{9,10,11},11->{9,10},12->{12,15,16,17},15->{9,10,11},16->{9,10,11},17->{9,10},21->{}
,22->{12,16}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, 121) (< 9,0,E>, E) (< 9,0,F>, 111) (< 9,0,G>, G) (< 9,0,H>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, 121) (<10,0,E>, E) (<10,0,F>, 111) (<10,0,G>, G) (<10,0,H>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
+ Applied Processor:
CombineProcessor [9,10,11,12,15,16,17,21,22]
+ Details:
We combined rules [9,10] to obtain the rule 23 .
* Step 22: CombineProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (595 + 6*A,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (200 + 2*A,1)
15. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 3
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
16. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [A + 11*D >= 112 (1,1)
&& D >= 2
&& 121 >= A + 11*D
&& 122 >= A + 11*D
&& 11*D >= 22
&& H = A
&& B = C
&& 11 + F = A + 11*D]
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
23. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [(D >= 2 || D >= 3) (400 + 4*A,2)
&& (D >= 2 || 110 >= F)
&& (D >= 2 || D >= 2)
&& (D >= 2 || F >= 102)
&& (D >= 2 || 111 >= F)
&& (D >= 2 || 10 + F >= A + 11*D)
&& (D >= 2 || 89 >= A)
&& (D >= 2 || H = A)
&& (D >= 2 || B = C)
&& (110 >= F || D >= 3)
&& (110 >= F || 110 >= F)
&& (110 >= F || D >= 2)
&& (110 >= F || F >= 102)
&& (110 >= F || 111 >= F)
&& (110 >= F || 10 + F >= A + 11*D)
&& (110 >= F || 89 >= A)
&& (110 >= F || H = A)
&& (110 >= F || B = C)
&& (F >= 102 || D >= 3)
&& (F >= 102 || 110 >= F)
&& (F >= 102 || D >= 2)
&& (F >= 102 || F >= 102)
&& (F >= 102 || 111 >= F)
&& (F >= 102 || 10 + F >= A + 11*D)
&& (F >= 102 || 89 >= A)
&& (F >= 102 || H = A)
&& (F >= 102 || B = C)
&& (111 >= F || D >= 3)
&& (111 >= F || 110 >= F)
&& (111 >= F || D >= 2)
&& (111 >= F || F >= 102)
&& (111 >= F || 111 >= F)
&& (111 >= F || 10 + F >= A + 11*D)
&& (111 >= F || 89 >= A)
&& (111 >= F || H = A)
&& (111 >= F || B = C)
&& (10 + F >= A + 11*D || D >= 3)
&& (10 + F >= A + 11*D || 110 >= F)
&& (10 + F >= A + 11*D || D >= 2)
&& (10 + F >= A + 11*D || F >= 102)
&& (10 + F >= A + 11*D || 111 >= F)
&& (10 + F >= A + 11*D || 10 + F >= A + 11*D)
&& (10 + F >= A + 11*D || 89 >= A)
&& (10 + F >= A + 11*D || H = A)
&& (10 + F >= A + 11*D || B = C)
&& (89 >= A || D >= 3)
&& (89 >= A || 110 >= F)
&& (89 >= A || D >= 2)
&& (89 >= A || F >= 102)
&& (89 >= A || 111 >= F)
&& (89 >= A || 10 + F >= A + 11*D)
&& (89 >= A || 89 >= A)
&& (89 >= A || H = A)
&& (89 >= A || B = C)
&& (H = A || D >= 3)
&& (H = A || 110 >= F)
&& (H = A || D >= 2)
&& (H = A || F >= 102)
&& (H = A || 111 >= F)
&& (H = A || 10 + F >= A + 11*D)
&& (H = A || 89 >= A)
&& (H = A || H = A)
&& (H = A || B = C)
&& (B = C || D >= 3)
&& (B = C || 110 >= F)
&& (B = C || D >= 2)
&& (B = C || F >= 102)
&& (B = C || 111 >= F)
&& (B = C || 10 + F >= A + 11*D)
&& (B = C || 89 >= A)
&& (B = C || H = A)
&& (B = C || B = C)]
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[11->{11,23},12->{12,15,16,17},15->{11,23},16->{11,23},17->{11,23},21->{},22->{12,15,16,17},23->{11,23}]
Sizebounds:
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, 112) (<15,0,E>, E) (<15,0,F>, 111) (<15,0,G>, G) (<15,0,H>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, 112) (<16,0,E>, E) (<16,0,F>, 111) (<16,0,G>, G) (<16,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
(<23,0,A>, A) (<23,0,B>, C) (<23,0,C>, C) (<23,0,D>, 121) (<23,0,E>, E) (<23,0,F>, 111) (<23,0,G>, G) (<23,0,H>, A)
+ Applied Processor:
CombineProcessor [11,12,15,16,17,21,22,23]
+ Details:
We combined rules [15,16] to obtain the rule 24 .
* Step 23: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && D >= 2 && 121 >= A + 11*D && 89 >= A && F = 111 && H = A && B = C] (595 + 6*A,1)
12. lbl111(A,B,C,D,E,F,G,H) -> lbl111(A,B,C,1 + D,E,11 + F,G,H) [111 >= A + 11*D && 122 >= A + 11*D && 11*D >= 22 && H = A && B = C && 11 + F = A + 11*D] (200 + 2*A,1)
17. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,-1 + D,E,-9 + F,G,H) [D >= 3 && 11*D >= 22 && F = 111 && 11*D + H = 122 && B = C && A + 11*D = 122] (1,1)
21. start0(A,B,C,D,E,F,G,H) -> stop(A,-10 + A,C,1,E,A,G,A) [A >= 101 && C = C && E = E && G = G && A = A] (1,2)
22. start0(A,B,C,D,E,F,G,H) -> lbl111(A,C,C,2,E,11 + A,G,A) [100 >= A && C = C && E = E && G = G && A = A] (1,2)
23. lbl221(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [(D >= 2 || D >= 3) (400 + 4*A,2)
&& (D >= 2 || 110 >= F)
&& (D >= 2 || D >= 2)
&& (D >= 2 || F >= 102)
&& (D >= 2 || 111 >= F)
&& (D >= 2 || 10 + F >= A + 11*D)
&& (D >= 2 || 89 >= A)
&& (D >= 2 || H = A)
&& (D >= 2 || B = C)
&& (110 >= F || D >= 3)
&& (110 >= F || 110 >= F)
&& (110 >= F || D >= 2)
&& (110 >= F || F >= 102)
&& (110 >= F || 111 >= F)
&& (110 >= F || 10 + F >= A + 11*D)
&& (110 >= F || 89 >= A)
&& (110 >= F || H = A)
&& (110 >= F || B = C)
&& (F >= 102 || D >= 3)
&& (F >= 102 || 110 >= F)
&& (F >= 102 || D >= 2)
&& (F >= 102 || F >= 102)
&& (F >= 102 || 111 >= F)
&& (F >= 102 || 10 + F >= A + 11*D)
&& (F >= 102 || 89 >= A)
&& (F >= 102 || H = A)
&& (F >= 102 || B = C)
&& (111 >= F || D >= 3)
&& (111 >= F || 110 >= F)
&& (111 >= F || D >= 2)
&& (111 >= F || F >= 102)
&& (111 >= F || 111 >= F)
&& (111 >= F || 10 + F >= A + 11*D)
&& (111 >= F || 89 >= A)
&& (111 >= F || H = A)
&& (111 >= F || B = C)
&& (10 + F >= A + 11*D || D >= 3)
&& (10 + F >= A + 11*D || 110 >= F)
&& (10 + F >= A + 11*D || D >= 2)
&& (10 + F >= A + 11*D || F >= 102)
&& (10 + F >= A + 11*D || 111 >= F)
&& (10 + F >= A + 11*D || 10 + F >= A + 11*D)
&& (10 + F >= A + 11*D || 89 >= A)
&& (10 + F >= A + 11*D || H = A)
&& (10 + F >= A + 11*D || B = C)
&& (89 >= A || D >= 3)
&& (89 >= A || 110 >= F)
&& (89 >= A || D >= 2)
&& (89 >= A || F >= 102)
&& (89 >= A || 111 >= F)
&& (89 >= A || 10 + F >= A + 11*D)
&& (89 >= A || 89 >= A)
&& (89 >= A || H = A)
&& (89 >= A || B = C)
&& (H = A || D >= 3)
&& (H = A || 110 >= F)
&& (H = A || D >= 2)
&& (H = A || F >= 102)
&& (H = A || 111 >= F)
&& (H = A || 10 + F >= A + 11*D)
&& (H = A || 89 >= A)
&& (H = A || H = A)
&& (H = A || B = C)
&& (B = C || D >= 3)
&& (B = C || 110 >= F)
&& (B = C || D >= 2)
&& (B = C || F >= 102)
&& (B = C || 111 >= F)
&& (B = C || 10 + F >= A + 11*D)
&& (B = C || 89 >= A)
&& (B = C || H = A)
&& (B = C || B = C)]
24. lbl111(A,B,C,D,E,F,G,H) -> lbl221(A,B,C,D,E,1 + F,G,H) [(A + 11*D >= 112 || A + 11*D >= 112) (2,2)
&& (A + 11*D >= 112 || D >= 3)
&& (A + 11*D >= 112 || 121 >= A + 11*D)
&& (A + 11*D >= 112 || 122 >= A + 11*D)
&& (A + 11*D >= 112 || 11*D >= 22)
&& (A + 11*D >= 112 || H = A)
&& (A + 11*D >= 112 || B = C)
&& (A + 11*D >= 112 || 11 + F = A + 11*D)
&& (D >= 2 || A + 11*D >= 112)
&& (D >= 2 || D >= 3)
&& (D >= 2 || 121 >= A + 11*D)
&& (D >= 2 || 122 >= A + 11*D)
&& (D >= 2 || 11*D >= 22)
&& (D >= 2 || H = A)
&& (D >= 2 || B = C)
&& (D >= 2 || 11 + F = A + 11*D)
&& (121 >= A + 11*D || A + 11*D >= 112)
&& (121 >= A + 11*D || D >= 3)
&& (121 >= A + 11*D || 121 >= A + 11*D)
&& (121 >= A + 11*D || 122 >= A + 11*D)
&& (121 >= A + 11*D || 11*D >= 22)
&& (121 >= A + 11*D || H = A)
&& (121 >= A + 11*D || B = C)
&& (121 >= A + 11*D || 11 + F = A + 11*D)
&& (122 >= A + 11*D || A + 11*D >= 112)
&& (122 >= A + 11*D || D >= 3)
&& (122 >= A + 11*D || 121 >= A + 11*D)
&& (122 >= A + 11*D || 122 >= A + 11*D)
&& (122 >= A + 11*D || 11*D >= 22)
&& (122 >= A + 11*D || H = A)
&& (122 >= A + 11*D || B = C)
&& (122 >= A + 11*D || 11 + F = A + 11*D)
&& (11*D >= 22 || A + 11*D >= 112)
&& (11*D >= 22 || D >= 3)
&& (11*D >= 22 || 121 >= A + 11*D)
&& (11*D >= 22 || 122 >= A + 11*D)
&& (11*D >= 22 || 11*D >= 22)
&& (11*D >= 22 || H = A)
&& (11*D >= 22 || B = C)
&& (11*D >= 22 || 11 + F = A + 11*D)
&& (H = A || A + 11*D >= 112)
&& (H = A || D >= 3)
&& (H = A || 121 >= A + 11*D)
&& (H = A || 122 >= A + 11*D)
&& (H = A || 11*D >= 22)
&& (H = A || H = A)
&& (H = A || B = C)
&& (H = A || 11 + F = A + 11*D)
&& (B = C || A + 11*D >= 112)
&& (B = C || D >= 3)
&& (B = C || 121 >= A + 11*D)
&& (B = C || 122 >= A + 11*D)
&& (B = C || 11*D >= 22)
&& (B = C || H = A)
&& (B = C || B = C)
&& (B = C || 11 + F = A + 11*D)
&& (11 + F = A + 11*D || A + 11*D >= 112)
&& (11 + F = A + 11*D || D >= 3)
&& (11 + F = A + 11*D || 121 >= A + 11*D)
&& (11 + F = A + 11*D || 122 >= A + 11*D)
&& (11 + F = A + 11*D || 11*D >= 22)
&& (11 + F = A + 11*D || H = A)
&& (11 + F = A + 11*D || B = C)
&& (11 + F = A + 11*D || 11 + F = A + 11*D)]
Signature:
{(lbl111,8);(lbl161,8);(lbl221,8);(start,8);(start0,8);(stop,8)}
Flow Graph:
[11->{11,23},12->{12,17,24},17->{11,23},21->{},22->{12,17,24},23->{11,23},24->{11,23}]
Sizebounds:
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, 120) (<11,0,E>, E) (<11,0,F>, 102) (<11,0,G>, G) (<11,0,H>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, 112) (<12,0,E>, E) (<12,0,F>, 111) (<12,0,G>, G) (<12,0,H>, A)
(<17,0,A>, A) (<17,0,B>, C) (<17,0,C>, C) (<17,0,D>, 114) (<17,0,E>, E) (<17,0,F>, 102) (<17,0,G>, G) (<17,0,H>, A)
(<21,0,A>, A) (<21,0,B>, 10 + A) (<21,0,C>, C) (<21,0,D>, 1) (<21,0,E>, E) (<21,0,F>, A) (<21,0,G>, G) (<21,0,H>, A)
(<22,0,A>, A) (<22,0,B>, C) (<22,0,C>, C) (<22,0,D>, 2) (<22,0,E>, E) (<22,0,F>, 11 + A) (<22,0,G>, G) (<22,0,H>, A)
(<23,0,A>, A) (<23,0,B>, C) (<23,0,C>, C) (<23,0,D>, 121) (<23,0,E>, E) (<23,0,F>, 111) (<23,0,G>, G) (<23,0,H>, A)
(<24,0,A>, A) (<24,0,B>, C) (<24,0,C>, C) (<24,0,D>, 112) (<24,0,E>, E) (<24,0,F>, 111) (<24,0,G>, G) (<24,0,H>, A)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))