WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G,H,I) -> f17(0,J,K,0,E,F,G,H,I) True (1,1)
1. f17(A,B,C,D,E,F,G,H,I) -> f17(A,B,C,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,B,C,D,E,F,G,H,I) -> f45(1 + A,B,C,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,B,C,D,E,F,G,H,I) -> f83(1 + A,B,C,D,E,F,G,H,I) [49 >= A] (?,1)
9. f83(A,B,C,D,E,F,G,H,I) -> f93(A,B,C,D,E,F,G,H,I) [A >= 50] (?,1)
10. f75(A,B,C,D,E,F,G,H,I) -> f83(0,B,C,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,B,C,D,E,F,G,H,I) -> f45(0,B,C,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,0,F,G,H,I) [D >= 50] (?,1)
Signature:
{(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)}
Flow Graph:
[0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9}
,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [B,C] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
9. f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [A >= 50] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (?,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9}
,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, 0, .= 0) (< 0,0,D>, 0, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) (< 0,0,G>, G, .= 0) (< 0,0,H>, H, .= 0) (< 0,0,I>, I, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,D>, 1 + D, .+ 1) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) (< 1,0,G>, G, .= 0) (< 1,0,H>, H, .= 0) (< 1,0,I>, I, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, 1 + E, .+ 1) (< 2,0,F>, F, .= 0) (< 2,0,G>, G, .= 0) (< 2,0,H>, H, .= 0) (< 2,0,I>, I, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, 1 + F, .+ 1) (< 3,0,G>, G, .= 0) (< 3,0,H>, H, .= 0) (< 3,0,I>, I, .= 0)
(< 4,0,A>, 1 + A, .+ 1) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) (< 4,0,G>, G, .= 0) (< 4,0,H>, H, .= 0) (< 4,0,I>, I, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, F, .= 0) (< 5,0,G>, 1 + G, .+ 1) (< 5,0,H>, H, .= 0) (< 5,0,I>, I, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 6,0,F>, F, .= 0) (< 6,0,G>, G, .= 0) (< 6,0,H>, 1 + H, .+ 1) (< 6,0,I>, I, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0) (< 7,0,H>, H, .= 0) (< 7,0,I>, 1 + I, .+ 1)
(< 8,0,A>, 1 + A, .+ 1) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0) (< 8,0,I>, I, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0) (< 9,0,G>, G, .= 0) (< 9,0,H>, H, .= 0) (< 9,0,I>, I, .= 0)
(<10,0,A>, 0, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0) (<10,0,G>, G, .= 0) (<10,0,H>, H, .= 0) (<10,0,I>, I, .= 0)
(<11,0,A>, A, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0) (<11,0,I>, 0, .= 0)
(<12,0,A>, A, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, F, .= 0) (<12,0,G>, G, .= 0) (<12,0,H>, 0, .= 0) (<12,0,I>, I, .= 0)
(<13,0,A>, A, .= 0) (<13,0,D>, D, .= 0) (<13,0,E>, E, .= 0) (<13,0,F>, F, .= 0) (<13,0,G>, 0, .= 0) (<13,0,H>, H, .= 0) (<13,0,I>, I, .= 0)
(<14,0,A>, 0, .= 0) (<14,0,D>, D, .= 0) (<14,0,E>, E, .= 0) (<14,0,F>, F, .= 0) (<14,0,G>, G, .= 0) (<14,0,H>, H, .= 0) (<14,0,I>, I, .= 0)
(<15,0,A>, A, .= 0) (<15,0,D>, D, .= 0) (<15,0,E>, E, .= 0) (<15,0,F>, 0, .= 0) (<15,0,G>, G, .= 0) (<15,0,H>, H, .= 0) (<15,0,I>, I, .= 0)
(<16,0,A>, A, .= 0) (<16,0,D>, D, .= 0) (<16,0,E>, 0, .= 0) (<16,0,F>, F, .= 0) (<16,0,G>, G, .= 0) (<16,0,H>, H, .= 0) (<16,0,I>, I, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
9. f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [A >= 50] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (?,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9}
,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 0,0,G>, ?) (< 0,0,H>, ?) (< 0,0,I>, ?)
(< 1,0,A>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 1,0,G>, ?) (< 1,0,H>, ?) (< 1,0,I>, ?)
(< 2,0,A>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 2,0,G>, ?) (< 2,0,H>, ?) (< 2,0,I>, ?)
(< 3,0,A>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 3,0,G>, ?) (< 3,0,H>, ?) (< 3,0,I>, ?)
(< 4,0,A>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 4,0,G>, ?) (< 4,0,H>, ?) (< 4,0,I>, ?)
(< 5,0,A>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?) (< 5,0,I>, ?)
(< 6,0,A>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 6,0,H>, ?) (< 6,0,I>, ?)
(< 7,0,A>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?) (< 7,0,I>, ?)
(< 8,0,A>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?) (< 8,0,I>, ?)
(< 9,0,A>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?) (< 9,0,G>, ?) (< 9,0,H>, ?) (< 9,0,I>, ?)
(<10,0,A>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, ?) (<10,0,I>, ?)
(<11,0,A>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?) (<11,0,I>, ?)
(<12,0,A>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, ?) (<12,0,I>, ?)
(<13,0,A>, ?) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?) (<13,0,I>, ?)
(<14,0,A>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?) (<14,0,I>, ?)
(<15,0,A>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<15,0,F>, ?) (<15,0,G>, ?) (<15,0,H>, ?) (<15,0,I>, ?)
(<16,0,A>, ?) (<16,0,D>, ?) (<16,0,E>, ?) (<16,0,F>, ?) (<16,0,G>, ?) (<16,0,H>, ?) (<16,0,I>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 50) (< 9,0,H>, 50) (< 9,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
9. f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [A >= 50] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (?,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9}
,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 50) (< 9,0,H>, 50) (< 9,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,16)
,(10,9)
,(11,10)
,(12,11)
,(13,12)
,(14,13)
,(15,14)
,(16,15)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
9. f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [A >= 50] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (?,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8}
,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(< 9,0,A>, 50) (< 9,0,D>, 50) (< 9,0,E>, 50) (< 9,0,F>, 50) (< 9,0,G>, 50) (< 9,0,H>, 50) (< 9,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [9]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (?,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f17) = 1
p(f27) = 0
p(f37) = 0
p(f45) = 0
p(f55) = 0
p(f65) = 0
p(f75) = 0
p(f83) = 0
The following rules are strictly oriented:
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 1
> 0
= f27(A,D,0,F,G,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 1
>= 1
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 1
>= 1
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 0
>= 0
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 0
>= 0
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 0
>= 0
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 0
>= 0
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 0
>= 0
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 0
>= 0
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 0
>= 0
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 0
>= 0
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 0
>= 0
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 0
>= 0
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 0
>= 0
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 0
>= 0
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 0
>= 0
= f37(A,D,E,0,G,H,I)
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (?,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50
p(f37) = 50 + -1*x4
p(f45) = 50 + -1*x4
p(f55) = 50 + -1*x4
p(f65) = 50 + -1*x4
p(f75) = 50 + -1*x4
p(f83) = 50 + -1*x4
The following rules are strictly oriented:
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50 + -1*F
> 49 + -1*F
= f37(A,D,E,1 + F,G,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,1 + E,F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50 + -1*F
>= 50 + -1*F
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 8: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (?,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (?,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50
p(f37) = 50
p(f45) = 50
p(f55) = 50 + -1*x5
p(f65) = 50 + -1*x5
p(f75) = 50 + -1*x5
p(f83) = 50 + -1*x5
The following rules are strictly oriented:
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 50 + -1*G
> 49 + -1*G
= f55(A,D,E,F,1 + G,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f45(1 + A,D,E,F,G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 50 + -1*G
>= 50 + -1*G
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*G
>= 50 + -1*G
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 50 + -1*G
>= 50 + -1*G
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*G
>= 50 + -1*G
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 50 + -1*G
>= 50 + -1*G
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 50 + -1*G
>= 50 + -1*G
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 10: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (?,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ 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,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (?,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50
p(f37) = 50
p(f45) = 50
p(f55) = 50
p(f65) = 50
p(f75) = 50 + -1*x7
p(f83) = 50 + -1*x7
The following rules are strictly oriented:
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*I
> 49 + -1*I
= f75(A,D,E,F,G,H,1 + I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 50
>= 50
= f65(A,D,E,F,G,1 + H,I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 50 + -1*I
>= 50 + -1*I
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*I
>= 50 + -1*I
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 50
>= 50
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 12: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (?,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 13: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (?,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 51
p(f17) = 51
p(f27) = 51
p(f37) = 50
p(f45) = 50
p(f55) = 50
p(f65) = 50
p(f75) = 50
p(f83) = 50 + -1*x1
The following rules are strictly oriented:
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 50 + -1*A
> 49 + -1*A
= f83(1 + A,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 51
> 50
= f37(A,D,E,0,G,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 51
>= 51
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 51
>= 51
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 51
>= 51
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 50
>= 50
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 50
>= 50
= f75(A,D,E,F,G,H,1 + I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 50
>= 50
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 50
>= 50
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f45(0,D,E,F,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 51
>= 51
= f27(A,D,0,F,G,H,I)
* Step 14: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (?,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50 + -1*x3
p(f37) = -1*x3
p(f45) = -1*x3
p(f55) = -1*x3
p(f65) = -1*x3
p(f75) = -1*x3
p(f83) = -1*x3
The following rules are strictly oriented:
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50 + -1*E
> 49 + -1*E
= f27(A,D,1 + E,F,G,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = -1*E
>= -1*E
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50 + -1*E
>= -1*E
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 15: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (?,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (50,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50 + -1*x2
p(f27) = -1*x2
p(f37) = -1*x2
p(f45) = -1*x2
p(f55) = -1*x2
p(f65) = -1*x2
p(f75) = -1*x2
p(f83) = -1*x2
The following rules are strictly oriented:
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50 + -1*D
> 49 + -1*D
= f17(A,1 + D,E,F,G,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = -1*D
>= -1*D
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50 + -1*D
>= -1*D
= f27(A,D,0,F,G,H,I)
* Step 16: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (50,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (50,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (?,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50
p(f37) = 50
p(f45) = 50
p(f55) = 50
p(f65) = 2
p(f75) = 1
p(f83) = 1
The following rules are strictly oriented:
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 2
> 1
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 50
> 2
= f65(A,D,E,F,G,0,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 2
>= 2
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 1
>= 1
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 1
>= 1
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 1
>= 1
= f83(0,D,E,F,G,H,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 17: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (50,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (50,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (?,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (50,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50
p(f37) = 50
p(f45) = 50
p(f55) = 50
p(f65) = 50 + -1*x6
p(f75) = 50 + -1*x6
p(f83) = 50 + -1*x6
The following rules are strictly oriented:
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 50 + -1*H
> 49 + -1*H
= f65(A,D,E,F,G,1 + H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,1 + G,H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*H
>= 50 + -1*H
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 50 + -1*H
>= 50 + -1*H
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 50 + -1*H
>= 50 + -1*H
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 50 + -1*H
>= 50 + -1*H
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 50
>= 50
= f65(A,D,E,F,G,0,I)
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f55(A,D,E,F,0,H,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 18: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (50,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (50,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (50,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (50,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (?,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 50
p(f17) = 50
p(f27) = 50
p(f37) = 50
p(f45) = 50
p(f55) = 49
p(f65) = 49
p(f75) = 49
p(f83) = 49
The following rules are strictly oriented:
[A >= 50] ==>
f45(A,D,E,F,G,H,I) = 50
> 49
= f55(A,D,E,F,0,H,I)
The following rules are weakly oriented:
True ==>
f0(A,D,E,F,G,H,I) = 50
>= 50
= f17(0,0,E,F,G,H,I)
[49 >= D] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f17(A,1 + D,E,F,G,H,I)
[49 >= E] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,1 + E,F,G,H,I)
[49 >= F] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,1 + F,G,H,I)
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50
>= 50
= f45(1 + A,D,E,F,G,H,I)
[49 >= G] ==>
f55(A,D,E,F,G,H,I) = 49
>= 49
= f55(A,D,E,F,1 + G,H,I)
[49 >= H] ==>
f65(A,D,E,F,G,H,I) = 49
>= 49
= f65(A,D,E,F,G,1 + H,I)
[49 >= I] ==>
f75(A,D,E,F,G,H,I) = 49
>= 49
= f75(A,D,E,F,G,H,1 + I)
[49 >= A] ==>
f83(A,D,E,F,G,H,I) = 49
>= 49
= f83(1 + A,D,E,F,G,H,I)
[I >= 50] ==>
f75(A,D,E,F,G,H,I) = 49
>= 49
= f83(0,D,E,F,G,H,I)
[H >= 50] ==>
f65(A,D,E,F,G,H,I) = 49
>= 49
= f75(A,D,E,F,G,H,0)
[G >= 50] ==>
f55(A,D,E,F,G,H,I) = 49
>= 49
= f65(A,D,E,F,G,0,I)
[F >= 50] ==>
f37(A,D,E,F,G,H,I) = 50
>= 50
= f45(0,D,E,F,G,H,I)
[E >= 50] ==>
f27(A,D,E,F,G,H,I) = 50
>= 50
= f37(A,D,E,0,G,H,I)
[D >= 50] ==>
f17(A,D,E,F,G,H,I) = 50
>= 50
= f27(A,D,0,F,G,H,I)
* Step 19: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (50,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (50,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (?,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (50,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (50,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (50,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [4], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f45) = 50 + -1*x1
The following rules are strictly oriented:
[49 >= A] ==>
f45(A,D,E,F,G,H,I) = 50 + -1*A
> 49 + -1*A
= f45(1 + A,D,E,F,G,H,I)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
* Step 20: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1)
1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [49 >= D] (50,1)
2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [49 >= E] (50,1)
3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [49 >= F] (50,1)
4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [49 >= A] (2500,1)
5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [49 >= G] (50,1)
6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [49 >= H] (50,1)
7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [49 >= I] (50,1)
8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [49 >= A] (51,1)
10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 50] (50,1)
11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 50] (50,1)
12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 50] (50,1)
13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [A >= 50] (50,1)
14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 50] (50,1)
15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 50] (51,1)
16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 50] (1,1)
Signature:
{(f0,7);(f17,7);(f27,7);(f37,7);(f45,7);(f55,7);(f65,7);(f75,7);(f83,7);(f93,7)}
Flow Graph:
[0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8},10->{8},11->{7}
,12->{6},13->{5},14->{4},15->{3},16->{2}]
Sizebounds:
(< 0,0,A>, 0) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H) (< 0,0,I>, I)
(< 1,0,A>, 0) (< 1,0,D>, 50) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H) (< 1,0,I>, I)
(< 2,0,A>, 0) (< 2,0,D>, 50) (< 2,0,E>, 50) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H) (< 2,0,I>, I)
(< 3,0,A>, 0) (< 3,0,D>, 50) (< 3,0,E>, 50) (< 3,0,F>, 50) (< 3,0,G>, G) (< 3,0,H>, H) (< 3,0,I>, I)
(< 4,0,A>, 50) (< 4,0,D>, 50) (< 4,0,E>, 50) (< 4,0,F>, 50) (< 4,0,G>, G) (< 4,0,H>, H) (< 4,0,I>, I)
(< 5,0,A>, 50) (< 5,0,D>, 50) (< 5,0,E>, 50) (< 5,0,F>, 50) (< 5,0,G>, 50) (< 5,0,H>, H) (< 5,0,I>, I)
(< 6,0,A>, 50) (< 6,0,D>, 50) (< 6,0,E>, 50) (< 6,0,F>, 50) (< 6,0,G>, 50) (< 6,0,H>, 50) (< 6,0,I>, I)
(< 7,0,A>, 50) (< 7,0,D>, 50) (< 7,0,E>, 50) (< 7,0,F>, 50) (< 7,0,G>, 50) (< 7,0,H>, 50) (< 7,0,I>, 50)
(< 8,0,A>, 50) (< 8,0,D>, 50) (< 8,0,E>, 50) (< 8,0,F>, 50) (< 8,0,G>, 50) (< 8,0,H>, 50) (< 8,0,I>, 50)
(<10,0,A>, 0) (<10,0,D>, 50) (<10,0,E>, 50) (<10,0,F>, 50) (<10,0,G>, 50) (<10,0,H>, 50) (<10,0,I>, 50)
(<11,0,A>, 50) (<11,0,D>, 50) (<11,0,E>, 50) (<11,0,F>, 50) (<11,0,G>, 50) (<11,0,H>, 50) (<11,0,I>, 0)
(<12,0,A>, 50) (<12,0,D>, 50) (<12,0,E>, 50) (<12,0,F>, 50) (<12,0,G>, 50) (<12,0,H>, 0) (<12,0,I>, I)
(<13,0,A>, 50) (<13,0,D>, 50) (<13,0,E>, 50) (<13,0,F>, 50) (<13,0,G>, 0) (<13,0,H>, H) (<13,0,I>, I)
(<14,0,A>, 0) (<14,0,D>, 50) (<14,0,E>, 50) (<14,0,F>, 50) (<14,0,G>, G) (<14,0,H>, H) (<14,0,I>, I)
(<15,0,A>, 0) (<15,0,D>, 50) (<15,0,E>, 50) (<15,0,F>, 0) (<15,0,G>, G) (<15,0,H>, H) (<15,0,I>, I)
(<16,0,A>, 0) (<16,0,D>, 50) (<16,0,E>, 0) (<16,0,F>, F) (<16,0,G>, G) (<16,0,H>, H) (<16,0,I>, I)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))