WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D) -> stop(A,B,C,D) [A >= 30 && B = C && D = A] (?,1)
1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [C >= A && 29 >= A && B = C && D = A] (?,1)
2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] (?,1)
3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (?,1)
4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1)
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[0->{},1->{4,5,6,7},2->{8,9,10},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8
,9,10},10->{8,9,10},11->{0,1,2,3}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, 10 + B, .+ 10) (< 1,0,C>, C, .= 0) (< 1,0,D>, 2 + D, .+ 2)
(< 2,0,A>, A, .= 0) (< 2,0,B>, 35, .= 35) (< 2,0,C>, C, .= 0) (< 2,0,D>, 30, .= 30)
(< 3,0,A>, A, .= 0) (< 3,0,B>, 2 + B, .+ 2) (< 3,0,C>, C, .= 0) (< 3,0,D>, 1 + D, .+ 1)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, 10 + B, .+ 10) (< 5,0,C>, C, .= 0) (< 5,0,D>, 31 + D, .+ 31)
(< 6,0,A>, A, .= 0) (< 6,0,B>, 35, .= 35) (< 6,0,C>, C, .= 0) (< 6,0,D>, 30, .= 30)
(< 7,0,A>, A, .= 0) (< 7,0,B>, 7 + B, .+ 7) (< 7,0,C>, C, .= 0) (< 7,0,D>, 30 + D, .+ 30)
(< 8,0,A>, A, .= 0) (< 8,0,B>, 10 + B, .+ 10) (< 8,0,C>, C, .= 0) (< 8,0,D>, 2 + D, .+ 2)
(< 9,0,A>, A, .= 0) (< 9,0,B>, 13 + B, .+ 13) (< 9,0,C>, C, .= 0) (< 9,0,D>, 1 + D, .+ 1)
(<10,0,A>, A, .= 0) (<10,0,B>, 2 + B, .+ 2) (<10,0,C>, C, .= 0) (<10,0,D>, 1 + D, .+ 1)
(<11,0,A>, A, .= 0) (<11,0,B>, C, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, A, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D) -> stop(A,B,C,D) [A >= 30 && B = C && D = A] (?,1)
1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [C >= A && 29 >= A && B = C && D = A] (?,1)
2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] (?,1)
3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (?,1)
4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1)
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[0->{},1->{4,5,6,7},2->{8,9,10},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8
,9,10},10->{8,9,10},11->{0,1,2,3}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, A)
(< 1,0,A>, A) (< 1,0,B>, 10 + C) (< 1,0,C>, C) (< 1,0,D>, 2 + A)
(< 2,0,A>, A) (< 2,0,B>, 35) (< 2,0,C>, C) (< 2,0,D>, 30)
(< 3,0,A>, A) (< 3,0,B>, 2 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, ?)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A)
* Step 3: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D) -> stop(A,B,C,D) [A >= 30 && B = C && D = A] (?,1)
1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [C >= A && 29 >= A && B = C && D = A] (?,1)
2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] (?,1)
3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (?,1)
4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1)
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[0->{},1->{4,5,6,7},2->{8,9,10},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8
,9,10},10->{8,9,10},11->{0,1,2,3}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, A)
(< 1,0,A>, A) (< 1,0,B>, 10 + C) (< 1,0,C>, C) (< 1,0,D>, 2 + A)
(< 2,0,A>, A) (< 2,0,B>, 35) (< 2,0,C>, C) (< 2,0,D>, 30)
(< 3,0,A>, A) (< 3,0,B>, 2 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, ?)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, A)
+ Applied Processor:
ChainProcessor False [0,1,2,3,4,5,6,7,8,9,10,11]
+ Details:
We chained rule 11 to obtain the rules [12,13,14,15] .
* Step 4: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D) -> stop(A,B,C,D) [A >= 30 && B = C && D = A] (?,1)
1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [C >= A && 29 >= A && B = C && D = A] (?,1)
2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] (?,1)
3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (?,1)
4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1)
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[0->{},1->{4,5,6,7},2->{8,9,10},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8
,9,10},10->{8,9,10},12->{},13->{4,5,6,7},14->{8,9,10},15->{8,9,10}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, A)
(< 1,0,A>, A) (< 1,0,B>, 10 + C) (< 1,0,C>, C) (< 1,0,D>, 2 + A)
(< 2,0,A>, A) (< 2,0,B>, 35) (< 2,0,C>, C) (< 2,0,D>, 30)
(< 3,0,A>, A) (< 3,0,B>, 2 + C) (< 3,0,C>, C) (< 3,0,D>, 1 + A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, ?)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [0,1,2,3]
* Step 5: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1)
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8,9,10},10->{8,9,10},12->{},13->{4,5,6,7}
,14->{8,9,10},15->{8,9,10}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, ?)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(6,10),(8,5),(9,10),(14,10)]
* Step 6: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1)
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9},10->{8,9,10},12->{},13->{4,5,6,7},14->{8,9}
,15->{8,9,10}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, ?)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [4]
* Step 7: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, ?)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 5,0,A>, A, .= 0) (< 5,0,B>, 10 + B, .+ 10) (< 5,0,C>, C, .= 0) (< 5,0,D>, 31 + D, .+ 31)
(< 6,0,A>, A, .= 0) (< 6,0,B>, 35, .= 35) (< 6,0,C>, C, .= 0) (< 6,0,D>, 30, .= 30)
(< 7,0,A>, A, .= 0) (< 7,0,B>, 7 + B, .+ 7) (< 7,0,C>, C, .= 0) (< 7,0,D>, 30 + D, .+ 30)
(< 8,0,A>, A, .= 0) (< 8,0,B>, 10 + B, .+ 10) (< 8,0,C>, C, .= 0) (< 8,0,D>, 2 + D, .+ 2)
(< 9,0,A>, A, .= 0) (< 9,0,B>, 13 + B, .+ 13) (< 9,0,C>, C, .= 0) (< 9,0,D>, 1 + D, .+ 1)
(<10,0,A>, A, .= 0) (<10,0,B>, 2 + B, .+ 2) (<10,0,C>, C, .= 0) (<10,0,D>, 1 + D, .+ 1)
(<12,0,A>, A, .= 0) (<12,0,B>, C, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, A, .= 0)
(<13,0,A>, A, .= 0) (<13,0,B>, 10 + C, .+ 10) (<13,0,C>, C, .= 0) (<13,0,D>, 2 + A + C, .* 2)
(<14,0,A>, A, .= 0) (<14,0,B>, 35, .= 35) (<14,0,C>, C, .= 0) (<14,0,D>, 30, .= 30)
(<15,0,A>, A, .= 0) (<15,0,B>, 2 + C, .+ 2) (<15,0,C>, C, .= 0) (<15,0,D>, 1 + A, .+ 1)
* Step 8: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
* Step 9: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 5 : [C >= A
&& C >= A] 6 : [A = A] 7 : [A = A] 8 : [A = A] 9 : [A = A] 10 : [A = A] 12 : True 13 : True 14 : True 15 : True .
* Step 10: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl151) = 146 + -5*x1 + -1*x3 + -1*x4
p(lbl171) = 146 + -5*x1 + -1*x3 + -1*x4
p(start0) = 145 + -6*x1 + -1*x3
p(stop) = 145 + -1*x2 + -6*x4
The following rules are strictly oriented:
[D >= 1 + B ==>
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 146 + -5*A + -1*C + -1*D
> 145 + -5*A + -1*C + -1*D
= lbl151(A,2 + B,C,1 + D)
The following rules are weakly oriented:
[B >= D ==>
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 146 + -5*A + -1*C + -1*D
>= 144 + -5*A + -1*C + -1*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 146 + -5*A + -1*C + -1*D
>= 145 + -5*A + -1*C + -1*D
= lbl151(A,7 + B,C,1 + D)
[B >= D ==>
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 146 + -5*A + -1*C + -1*D
>= 144 + -5*A + -1*C + -1*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 146 + -5*A + -1*C + -1*D
>= 145 + -5*A + -1*C + -1*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 146 + -5*A + -1*C + -1*D
>= 145 + -5*A + -1*C + -1*D
= lbl151(A,2 + B,C,1 + D)
[A >= 30 && C = C && A = A] ==>
start0(A,B,C,D) = 145 + -6*A + -1*C
>= 145 + -6*A + -1*C
= stop(A,C,C,A)
[C >= A && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 145 + -6*A + -1*C
>= 144 + -6*A + -1*C
= lbl171(A,-10 + C,C,2 + A)
[A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 145 + -6*A + -1*C
>= 145 + -6*A + -1*C
= lbl151(A,7 + C,C,1 + A)
[A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 145 + -6*A + -1*C
>= 145 + -6*A + -1*C
= lbl151(A,2 + C,C,1 + A)
* Step 11: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl151) = 1218 + -41*x1 + -1*x3 + -1*x4
p(lbl171) = 1220 + -41*x1 + -1*x3 + -1*x4
p(start0) = 1218 + -42*x1 + -1*x3
p(stop) = 1218 + -1*x2 + -42*x4
The following rules are strictly oriented:
[D >= 1 + B ==>
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 1220 + -41*A + -1*C + -1*D
> 1217 + -41*A + -1*C + -1*D
= lbl151(A,7 + B,C,1 + D)
The following rules are weakly oriented:
[B >= D ==>
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 1220 + -41*A + -1*C + -1*D
>= 1218 + -41*A + -1*C + -1*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 1220 + -41*A + -1*C + -1*D
>= 1217 + -41*A + -1*C + -1*D
= lbl151(A,2 + B,C,1 + D)
[B >= D ==>
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 1218 + -41*A + -1*C + -1*D
>= 1218 + -41*A + -1*C + -1*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 1218 + -41*A + -1*C + -1*D
>= 1217 + -41*A + -1*C + -1*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 1218 + -41*A + -1*C + -1*D
>= 1217 + -41*A + -1*C + -1*D
= lbl151(A,2 + B,C,1 + D)
[A >= 30 && C = C && A = A] ==>
start0(A,B,C,D) = 1218 + -42*A + -1*C
>= 1218 + -42*A + -1*C
= stop(A,C,C,A)
[C >= A && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 1218 + -42*A + -1*C
>= 1218 + -42*A + -1*C
= lbl171(A,-10 + C,C,2 + A)
[A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 1218 + -42*A + -1*C
>= 1217 + -42*A + -1*C
= lbl151(A,7 + C,C,1 + A)
[A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 1218 + -42*A + -1*C
>= 1217 + -42*A + -1*C
= lbl151(A,2 + C,C,1 + A)
* Step 12: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (1218 + 42*A + C,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (?,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl151) = 209 + -5*x1 + -1*x3 + -1*x4
p(lbl171) = 211 + -5*x1 + -1*x3 + -1*x4
p(start0) = 209 + -6*x1 + -1*x3
p(stop) = 209 + -1*x2 + -6*x4
The following rules are strictly oriented:
[D >= 1 + B ==>
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 211 + -5*A + -1*C + -1*D
> 208 + -5*A + -1*C + -1*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 211 + -5*A + -1*C + -1*D
> 208 + -5*A + -1*C + -1*D
= lbl151(A,2 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 209 + -5*A + -1*C + -1*D
> 208 + -5*A + -1*C + -1*D
= lbl151(A,2 + B,C,1 + D)
[A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 209 + -6*A + -1*C
> 208 + -6*A + -1*C
= lbl151(A,7 + C,C,1 + A)
[A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 209 + -6*A + -1*C
> 208 + -6*A + -1*C
= lbl151(A,2 + C,C,1 + A)
The following rules are weakly oriented:
[B >= D ==>
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 211 + -5*A + -1*C + -1*D
>= 209 + -5*A + -1*C + -1*D
= lbl171(A,-10 + B,C,2 + D)
[B >= D ==>
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 209 + -5*A + -1*C + -1*D
>= 209 + -5*A + -1*C + -1*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 209 + -5*A + -1*C + -1*D
>= 208 + -5*A + -1*C + -1*D
= lbl151(A,7 + B,C,1 + D)
[A >= 30 && C = C && A = A] ==>
start0(A,B,C,D) = 209 + -6*A + -1*C
>= 209 + -6*A + -1*C
= stop(A,C,C,A)
[C >= A && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 209 + -6*A + -1*C
>= 209 + -6*A + -1*C
= lbl171(A,-10 + C,C,2 + A)
* Step 13: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (?,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl151) = 3584 + -103*x1 + -1*x2 + -11*x3 + -7*x4
p(lbl171) = 3577 + -103*x1 + -1*x2 + -11*x3 + -7*x4
p(start0) = 3575 + -110*x1 + -12*x3
p(stop) = 3575 + -12*x2 + -110*x4
The following rules are strictly oriented:
[D >= 1 + B ==>
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 3577 + -103*A + -1*B + -11*C + -7*D
> 3570 + -103*A + -1*B + -11*C + -7*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 3577 + -103*A + -1*B + -11*C + -7*D
> 3575 + -103*A + -1*B + -11*C + -7*D
= lbl151(A,2 + B,C,1 + D)
[D >= 1 + B ==>
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 3584 + -103*A + -1*B + -11*C + -7*D
> 3570 + -103*A + -1*B + -11*C + -7*D
= lbl151(A,7 + B,C,1 + D)
[A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 3575 + -110*A + -12*C
> 3570 + -110*A + -12*C
= lbl151(A,7 + C,C,1 + A)
The following rules are weakly oriented:
[B >= D ==>
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 3577 + -103*A + -1*B + -11*C + -7*D
>= 3573 + -103*A + -1*B + -11*C + -7*D
= lbl171(A,-10 + B,C,2 + D)
[B >= D ==>
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 3584 + -103*A + -1*B + -11*C + -7*D
>= 3573 + -103*A + -1*B + -11*C + -7*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 3584 + -103*A + -1*B + -11*C + -7*D
>= 3575 + -103*A + -1*B + -11*C + -7*D
= lbl151(A,2 + B,C,1 + D)
[A >= 30 && C = C && A = A] ==>
start0(A,B,C,D) = 3575 + -110*A + -12*C
>= 3575 + -110*A + -12*C
= stop(A,C,C,A)
[C >= A && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 3575 + -110*A + -12*C
>= 3573 + -110*A + -12*C
= lbl171(A,-10 + C,C,2 + A)
[A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 3575 + -110*A + -12*C
>= 3575 + -110*A + -12*C
= lbl151(A,2 + C,C,1 + A)
* Step 14: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (3575 + 110*A + 12*C,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl151) = 1950 + -57*x1 + -7*x3 + -2*x4
p(lbl171) = 1952 + -57*x1 + -7*x3 + -2*x4
p(start0) = 1948 + -59*x1 + -7*x3
p(stop) = 1948 + -7*x2 + -59*x4
The following rules are strictly oriented:
[B >= D ==>
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 1950 + -57*A + -7*C + -2*D
> 1948 + -57*A + -7*C + -2*D
= lbl171(A,-10 + B,C,2 + D)
The following rules are weakly oriented:
[B >= D ==>
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 1952 + -57*A + -7*C + -2*D
>= 1948 + -57*A + -7*C + -2*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 1952 + -57*A + -7*C + -2*D
>= 1948 + -57*A + -7*C + -2*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 1952 + -57*A + -7*C + -2*D
>= 1948 + -57*A + -7*C + -2*D
= lbl151(A,2 + B,C,1 + D)
[D >= 1 + B ==>
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 1950 + -57*A + -7*C + -2*D
>= 1948 + -57*A + -7*C + -2*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 1950 + -57*A + -7*C + -2*D
>= 1948 + -57*A + -7*C + -2*D
= lbl151(A,2 + B,C,1 + D)
[A >= 30 && C = C && A = A] ==>
start0(A,B,C,D) = 1948 + -59*A + -7*C
>= 1948 + -59*A + -7*C
= stop(A,C,C,A)
[C >= A && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 1948 + -59*A + -7*C
>= 1948 + -59*A + -7*C
= lbl171(A,-10 + C,C,2 + A)
[A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 1948 + -59*A + -7*C
>= 1948 + -59*A + -7*C
= lbl151(A,7 + C,C,1 + A)
[A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 1948 + -59*A + -7*C
>= 1948 + -59*A + -7*C
= lbl151(A,2 + C,C,1 + A)
* Step 15: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (?,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (1948 + 59*A + 7*C,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (3575 + 110*A + 12*C,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl151) = 673 + -17*x1 + x2 + -1*x3 + -7*x4
p(lbl171) = 697 + -17*x1 + x2 + -1*x3 + -7*x4
p(start0) = 673 + -24*x1
p(stop) = 673 + -24*x4
The following rules are strictly oriented:
[B >= D ==>
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 697 + -17*A + B + -1*C + -7*D
> 673 + -17*A + B + -1*C + -7*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 697 + -17*A + B + -1*C + -7*D
> 673 + -17*A + B + -1*C + -7*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
lbl171(A,B,C,D) = 697 + -17*A + B + -1*C + -7*D
> 668 + -17*A + B + -1*C + -7*D
= lbl151(A,2 + B,C,1 + D)
The following rules are weakly oriented:
[B >= D ==>
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 673 + -17*A + B + -1*C + -7*D
>= 673 + -17*A + B + -1*C + -7*D
= lbl171(A,-10 + B,C,2 + D)
[D >= 1 + B ==>
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 673 + -17*A + B + -1*C + -7*D
>= 673 + -17*A + B + -1*C + -7*D
= lbl151(A,7 + B,C,1 + D)
[D >= 1 + B ==>
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
lbl151(A,B,C,D) = 673 + -17*A + B + -1*C + -7*D
>= 668 + -17*A + B + -1*C + -7*D
= lbl151(A,2 + B,C,1 + D)
[A >= 30 && C = C && A = A] ==>
start0(A,B,C,D) = 673 + -24*A
>= 673 + -24*A
= stop(A,C,C,A)
[C >= A && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 673 + -24*A
>= 673 + -24*A
= lbl171(A,-10 + C,C,2 + A)
[A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 673 + -24*A
>= 673 + -24*A
= lbl151(A,7 + C,C,1 + A)
[A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] ==>
start0(A,B,C,D) = 673 + -24*A
>= 668 + -24*A
= lbl151(A,2 + C,C,1 + A)
* Step 16: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (673 + 24*A,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (1948 + 59*A + 7*C,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (3575 + 110*A + 12*C,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
LoopRecurrenceProcessor [5]
+ Details:
Applying the recurrence pattern linear * f to the expression B-A yields the solution -1*A + B .
* Step 17: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (673 + 24*A,1)
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& B >= 6
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (145 + 6*A + C,1)
&& 5 >= B
&& 29 >= D
&& 29 >= A
&& B + 5*D >= 5*A + C
&& C + 7*D >= 24 + 7*A + B
&& 1674 + 7*B >= 35*A + 7*C + 19*D
&& 12 + B >= D]
8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [B >= D (1948 + 59*A + 7*C,1)
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [D >= 1 + B (3575 + 110*A + 12*C,1)
&& B >= 6
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [D >= 1 + B (209 + 6*A + C,1)
&& 5 >= B
&& 6*D >= 7 + 5*A + C
&& B + 5*D >= 7 + 5*A + C
&& D >= 1 + A
&& 29 >= A
&& 203 + B >= 5*A + C + 2*D
&& 1561 + 2*B >= 35*A + 7*C + 14*D
&& 23*B + 140*D >= 161 + 140*A + 28*C
&& 5719 + 23*B >= 140*A + 28*C + 56*D
&& 5 + D >= B
&& C + 7*D >= 7*A + B]
12. start0(A,B,C,D) -> stop(A,C,C,A) [A >= 30 && C = C && A = A] (1,2)
13. start0(A,B,C,D) -> lbl171(A,-10 + C,C,2 + A) [C >= A && 29 >= A && C = C && A = A] (1,2)
14. start0(A,B,C,D) -> lbl151(A,7 + C,C,1 + A) [A >= 1 + C && C >= 6 && 29 >= A && C = C && A = A] (1,2)
15. start0(A,B,C,D) -> lbl151(A,2 + C,C,1 + A) [A >= 1 + C && 5 >= C && 29 >= A && C = C && A = A] (1,2)
Signature:
{(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
Flow Graph:
[5->{5,6,7},6->{8,9},7->{8,9,10},8->{6,7},9->{8,9},10->{8,9,10},12->{},13->{5,6,7},14->{8,9},15->{8,9,10}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 217 + 7*A + 8*C) (< 5,0,C>, C) (< 5,0,D>, 31)
(< 6,0,A>, A) (< 6,0,B>, 35) (< 6,0,C>, C) (< 6,0,D>, 30)
(< 7,0,A>, A) (< 7,0,B>, 30) (< 7,0,C>, C) (< 7,0,D>, 30)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 7) (<10,0,C>, C) (<10,0,D>, 234 + C)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, A)
(<13,0,A>, A) (<13,0,B>, 10 + C) (<13,0,C>, C) (<13,0,D>, 2 + A + C)
(<14,0,A>, A) (<14,0,B>, 35) (<14,0,C>, C) (<14,0,D>, 30)
(<15,0,A>, A) (<15,0,B>, 2 + C) (<15,0,C>, C) (<15,0,D>, 1 + A)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))