WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G) -> f12(2,H,I,0,E,F,G) True (1,1)
1. f12(A,B,C,D,E,F,G) -> f15(A,B,C,D,0,F,G) [A >= 1 + D] (?,1)
2. f15(A,B,C,D,E,F,G) -> f15(A,B,C,D,1 + E,F,G) [A >= 1 + E] (?,1)
3. f23(A,B,C,D,E,F,G) -> f26(A,B,C,D,0,F,G) [A >= 1 + D] (?,1)
4. f26(A,B,C,D,E,F,G) -> f30(A,B,C,D,E,0,G) [A >= 1 + E] (?,1)
5. f30(A,B,C,D,E,F,G) -> f30(A,B,C,D,E,1 + F,G) [A >= 1 + F] (?,1)
6. f30(A,B,C,D,E,F,G) -> f26(A,B,C,D,1 + E,F,G) [F >= A] (?,1)
7. f26(A,B,C,D,E,F,G) -> f23(A,B,C,1 + D,E,F,G) [E >= A] (?,1)
8. f23(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,0) [D >= A] (?,1)
9. f23(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,1) [D >= A && 49 >= H] (?,1)
10. f23(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,1) [D >= A] (?,1)
11. f23(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,1) [D >= A && 42 >= H] (?,1)
12. f23(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,1) [D >= A && 21 >= H] (?,1)
13. f23(A,B,C,D,E,F,G) -> f52(A,B,C,D,E,F,1) [D >= A && 18 >= H] (?,1)
14. f15(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [E >= A] (?,1)
15. f12(A,B,C,D,E,F,G) -> f23(A,B,C,0,E,F,G) [D >= A] (?,1)
Signature:
{(f0,7);(f12,7);(f15,7);(f23,7);(f26,7);(f30,7);(f52,7)}
Flow Graph:
[0->{1,15},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8,9,10,11,12,13},8->{},9->{}
,10->{},11->{},12->{},13->{},14->{1,15},15->{3,8,9,10,11,12,13}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [B,C,G] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (?,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
8. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
9. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 49 >= H] (?,1)
10. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
11. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 42 >= H] (?,1)
12. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 21 >= H] (?,1)
13. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 18 >= H] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (?,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1,15},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8,9,10,11,12,13},8->{},9->{}
,10->{},11->{},12->{},13->{},14->{1,15},15->{3,8,9,10,11,12,13}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, 2, .= 2) (< 0,0,D>, 0, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,D>, D, .= 0) (< 1,0,E>, 0, .= 0) (< 1,0,F>, F, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, 1 + E, .+ 1) (< 2,0,F>, F, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, 0, .= 0) (< 3,0,F>, F, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, 0, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, 1 + F, .+ 1)
(< 6,0,A>, A, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, 1 + E, .+ 1) (< 6,0,F>, F, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,D>, 1 + D, .+ 1) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0)
(<10,0,A>, A, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0)
(<11,0,A>, A, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0)
(<12,0,A>, A, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, F, .= 0)
(<13,0,A>, A, .= 0) (<13,0,D>, D, .= 0) (<13,0,E>, E, .= 0) (<13,0,F>, F, .= 0)
(<14,0,A>, A, .= 0) (<14,0,D>, 1 + D, .+ 1) (<14,0,E>, E, .= 0) (<14,0,F>, F, .= 0)
(<15,0,A>, A, .= 0) (<15,0,D>, 0, .= 0) (<15,0,E>, E, .= 0) (<15,0,F>, F, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (?,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
8. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
9. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 49 >= H] (?,1)
10. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
11. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 42 >= H] (?,1)
12. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 21 >= H] (?,1)
13. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 18 >= H] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (?,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1,15},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8,9,10,11,12,13},8->{},9->{}
,10->{},11->{},12->{},13->{},14->{1,15},15->{3,8,9,10,11,12,13}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?)
(< 1,0,A>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?)
(< 2,0,A>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?)
(< 3,0,A>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?)
(< 4,0,A>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?)
(< 5,0,A>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?)
(< 6,0,A>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?)
(< 7,0,A>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?)
(< 8,0,A>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?)
(< 9,0,A>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?)
(<10,0,A>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?)
(<11,0,A>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?)
(<12,0,A>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?)
(<13,0,A>, ?) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?)
(<14,0,A>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?)
(<15,0,A>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<15,0,F>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(< 8,0,A>, 2) (< 8,0,D>, ?) (< 8,0,E>, 2 + E) (< 8,0,F>, ?)
(< 9,0,A>, 2) (< 9,0,D>, ?) (< 9,0,E>, 2 + E) (< 9,0,F>, ?)
(<10,0,A>, 2) (<10,0,D>, ?) (<10,0,E>, 2 + E) (<10,0,F>, ?)
(<11,0,A>, 2) (<11,0,D>, ?) (<11,0,E>, 2 + E) (<11,0,F>, ?)
(<12,0,A>, 2) (<12,0,D>, ?) (<12,0,E>, 2 + E) (<12,0,F>, ?)
(<13,0,A>, 2) (<13,0,D>, ?) (<13,0,E>, 2 + E) (<13,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (?,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
8. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
9. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 49 >= H] (?,1)
10. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
11. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 42 >= H] (?,1)
12. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 21 >= H] (?,1)
13. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 18 >= H] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (?,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1,15},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8,9,10,11,12,13},8->{},9->{}
,10->{},11->{},12->{},13->{},14->{1,15},15->{3,8,9,10,11,12,13}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(< 8,0,A>, 2) (< 8,0,D>, ?) (< 8,0,E>, 2 + E) (< 8,0,F>, ?)
(< 9,0,A>, 2) (< 9,0,D>, ?) (< 9,0,E>, 2 + E) (< 9,0,F>, ?)
(<10,0,A>, 2) (<10,0,D>, ?) (<10,0,E>, 2 + E) (<10,0,F>, ?)
(<11,0,A>, 2) (<11,0,D>, ?) (<11,0,E>, 2 + E) (<11,0,F>, ?)
(<12,0,A>, 2) (<12,0,D>, ?) (<12,0,E>, 2 + E) (<12,0,F>, ?)
(<13,0,A>, 2) (<13,0,D>, ?) (<13,0,E>, 2 + E) (<13,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,15)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (?,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
8. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
9. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 49 >= H] (?,1)
10. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A] (?,1)
11. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 42 >= H] (?,1)
12. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 21 >= H] (?,1)
13. f23(A,D,E,F) -> f52(A,D,E,F) [D >= A && 18 >= H] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (?,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8,9,10,11,12,13},8->{},9->{},10->{}
,11->{},12->{},13->{},14->{1,15},15->{3,8,9,10,11,12,13}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(< 8,0,A>, 2) (< 8,0,D>, ?) (< 8,0,E>, 2 + E) (< 8,0,F>, ?)
(< 9,0,A>, 2) (< 9,0,D>, ?) (< 9,0,E>, 2 + E) (< 9,0,F>, ?)
(<10,0,A>, 2) (<10,0,D>, ?) (<10,0,E>, 2 + E) (<10,0,F>, ?)
(<11,0,A>, 2) (<11,0,D>, ?) (<11,0,E>, 2 + E) (<11,0,F>, ?)
(<12,0,A>, 2) (<12,0,D>, ?) (<12,0,E>, 2 + E) (<12,0,F>, ?)
(<13,0,A>, 2) (<13,0,D>, ?) (<13,0,E>, 2 + E) (<13,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [8,9,10,11,12,13]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (?,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (?,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f12) = 1
p(f15) = 1
p(f23) = 0
p(f26) = 0
p(f30) = 0
The following rules are strictly oriented:
[D >= A] ==>
f12(A,D,E,F) = 1
> 0
= f23(A,0,E,F)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F) = 1
>= 1
= f12(2,0,E,F)
[A >= 1 + D] ==>
f12(A,D,E,F) = 1
>= 1
= f15(A,D,0,F)
[A >= 1 + E] ==>
f15(A,D,E,F) = 1
>= 1
= f15(A,D,1 + E,F)
[A >= 1 + D] ==>
f23(A,D,E,F) = 0
>= 0
= f26(A,D,0,F)
[A >= 1 + E] ==>
f26(A,D,E,F) = 0
>= 0
= f30(A,D,E,0)
[A >= 1 + F] ==>
f30(A,D,E,F) = 0
>= 0
= f30(A,D,E,1 + F)
[F >= A] ==>
f30(A,D,E,F) = 0
>= 0
= f26(A,D,1 + E,F)
[E >= A] ==>
f26(A,D,E,F) = 0
>= 0
= f23(A,1 + D,E,F)
[E >= A] ==>
f15(A,D,E,F) = 1
>= 1
= f12(A,1 + D,E,F)
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (?,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 4
p(f12) = 2 + x1
p(f15) = 2 + x1
p(f23) = 2 + x1 + -1*x2
p(f26) = 1 + x1 + -1*x2
p(f30) = 1 + x1 + -1*x2
The following rules are strictly oriented:
[A >= 1 + D] ==>
f23(A,D,E,F) = 2 + A + -1*D
> 1 + A + -1*D
= f26(A,D,0,F)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F) = 4
>= 4
= f12(2,0,E,F)
[A >= 1 + D] ==>
f12(A,D,E,F) = 2 + A
>= 2 + A
= f15(A,D,0,F)
[A >= 1 + E] ==>
f15(A,D,E,F) = 2 + A
>= 2 + A
= f15(A,D,1 + E,F)
[A >= 1 + E] ==>
f26(A,D,E,F) = 1 + A + -1*D
>= 1 + A + -1*D
= f30(A,D,E,0)
[A >= 1 + F] ==>
f30(A,D,E,F) = 1 + A + -1*D
>= 1 + A + -1*D
= f30(A,D,E,1 + F)
[F >= A] ==>
f30(A,D,E,F) = 1 + A + -1*D
>= 1 + A + -1*D
= f26(A,D,1 + E,F)
[E >= A] ==>
f26(A,D,E,F) = 1 + A + -1*D
>= 1 + A + -1*D
= f23(A,1 + D,E,F)
[E >= A] ==>
f15(A,D,E,F) = 2 + A
>= 2 + A
= f12(A,1 + D,E,F)
[D >= A] ==>
f12(A,D,E,F) = 2 + A
>= 2 + A
= f23(A,0,E,F)
* Step 8: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (?,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [1,14,2], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f12) = 2 + x1 + -1*x2
p(f15) = 1 + x1 + -1*x2
The following rules are strictly oriented:
[A >= 1 + D] ==>
f12(A,D,E,F) = 2 + A + -1*D
> 1 + A + -1*D
= f15(A,D,0,F)
The following rules are weakly oriented:
[A >= 1 + E] ==>
f15(A,D,E,F) = 1 + A + -1*D
>= 1 + A + -1*D
= f15(A,D,1 + E,F)
[E >= A] ==>
f15(A,D,E,F) = 1 + A + -1*D
>= 1 + A + -1*D
= f12(A,1 + D,E,F)
We use the following global sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (?,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [2], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f15) = x1 + -1*x3
The following rules are strictly oriented:
[A >= 1 + E] ==>
f15(A,D,E,F) = A + -1*E
> -1 + A + -1*E
= f15(A,D,1 + E,F)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
* Step 10: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (8,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (?,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 11: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (8,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (?,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (12,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [6,4,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f26) = 2 + x1 + -1*x3
p(f30) = 1 + x1 + -1*x3
The following rules are strictly oriented:
[A >= 1 + E] ==>
f26(A,D,E,F) = 2 + A + -1*E
> 1 + A + -1*E
= f30(A,D,E,0)
The following rules are weakly oriented:
[A >= 1 + F] ==>
f30(A,D,E,F) = 1 + A + -1*E
>= 1 + A + -1*E
= f30(A,D,E,1 + F)
[F >= A] ==>
f30(A,D,E,F) = 1 + A + -1*E
>= 1 + A + -1*E
= f26(A,D,1 + E,F)
We use the following global sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
* Step 12: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (8,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (16,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (?,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (12,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [3,7,6,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f23) = 1
p(f26) = 1
p(f30) = 2
The following rules are strictly oriented:
[F >= A] ==>
f30(A,D,E,F) = 2
> 1
= f26(A,D,1 + E,F)
The following rules are weakly oriented:
[A >= 1 + D] ==>
f23(A,D,E,F) = 1
>= 1
= f26(A,D,0,F)
[A >= 1 + F] ==>
f30(A,D,E,F) = 2
>= 2
= f30(A,D,E,1 + F)
[E >= A] ==>
f26(A,D,E,F) = 1
>= 1
= f23(A,1 + D,E,F)
We use the following global sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
* Step 13: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (8,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (16,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (33,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (?,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (12,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 14: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (8,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (16,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (?,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (33,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (37,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (12,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [7,4,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f23) = x1
p(f26) = x1
p(f30) = x1 + -1*x4
The following rules are strictly oriented:
[A >= 1 + F] ==>
f30(A,D,E,F) = A + -1*F
> -1 + A + -1*F
= f30(A,D,E,1 + F)
The following rules are weakly oriented:
[A >= 1 + E] ==>
f26(A,D,E,F) = A
>= A
= f30(A,D,E,0)
[E >= A] ==>
f26(A,D,E,F) = A
>= A
= f23(A,1 + D,E,F)
We use the following global sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
* Step 15: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F) -> f12(2,0,E,F) True (1,1)
1. f12(A,D,E,F) -> f15(A,D,0,F) [A >= 1 + D] (4,1)
2. f15(A,D,E,F) -> f15(A,D,1 + E,F) [A >= 1 + E] (8,1)
3. f23(A,D,E,F) -> f26(A,D,0,F) [A >= 1 + D] (4,1)
4. f26(A,D,E,F) -> f30(A,D,E,0) [A >= 1 + E] (16,1)
5. f30(A,D,E,F) -> f30(A,D,E,1 + F) [A >= 1 + F] (74,1)
6. f30(A,D,E,F) -> f26(A,D,1 + E,F) [F >= A] (33,1)
7. f26(A,D,E,F) -> f23(A,1 + D,E,F) [E >= A] (37,1)
14. f15(A,D,E,F) -> f12(A,1 + D,E,F) [E >= A] (12,1)
15. f12(A,D,E,F) -> f23(A,0,E,F) [D >= A] (1,1)
Signature:
{(f0,4);(f12,4);(f15,4);(f23,4);(f26,4);(f30,4);(f52,4)}
Flow Graph:
[0->{1},1->{2,14},2->{2,14},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3},14->{1,15},15->{3}]
Sizebounds:
(< 0,0,A>, 2) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F)
(< 1,0,A>, 2) (< 1,0,D>, 2) (< 1,0,E>, 0) (< 1,0,F>, F)
(< 2,0,A>, 2) (< 2,0,D>, 2) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, 2) (< 3,0,D>, 2) (< 3,0,E>, 0) (< 3,0,F>, ?)
(< 4,0,A>, 2) (< 4,0,D>, ?) (< 4,0,E>, 2) (< 4,0,F>, 0)
(< 5,0,A>, 2) (< 5,0,D>, ?) (< 5,0,E>, 2) (< 5,0,F>, 2)
(< 6,0,A>, 2) (< 6,0,D>, ?) (< 6,0,E>, 2) (< 6,0,F>, 2)
(< 7,0,A>, 2) (< 7,0,D>, ?) (< 7,0,E>, 2) (< 7,0,F>, ?)
(<14,0,A>, 2) (<14,0,D>, 2) (<14,0,E>, 2) (<14,0,F>, F)
(<15,0,A>, 2) (<15,0,D>, 0) (<15,0,E>, 2 + E) (<15,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))