WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G) -> f46(5,12,0,0,E,F,G) True (1,1)
1. f46(A,B,C,D,E,F,G) -> f46(A,B,C,1 + C,E,F,G) [A >= 1 + D && C = D] (?,1)
2. f46(A,B,C,D,E,F,G) -> f46(A,B,C,1 + D,E,F,G) [A >= 1 + D && C >= 1 + D] (?,1)
3. f46(A,B,C,D,E,F,G) -> f46(A,B,C,1 + D,E,F,G) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E,F,G) -> f57(A,B,C,D,0,F,G) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E,F,G) -> f57(A,B,C,D,1 + E,H,I) [B >= 1 + E] (?,1)
6. f68(A,B,C,D,E,F,G) -> f74(A,B,C,D,E,H,I) [B >= 1 + D] (?,1)
7. f68(A,B,C,D,E,F,G) -> f68(A,B,C,1 + D,E,H,I) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E,F,G) -> f78(A,B,C,1 + D,E,F,G) [A >= 1 + D] (?,1)
9. f78(A,B,C,D,E,F,G) -> f74(A,B,C,D,E,F,G) [D >= A] (?,1)
10. f68(A,B,C,D,E,F,G) -> f78(A,B,C,0,E,F,G) [D >= B] (?,1)
11. f57(A,B,C,D,E,F,G) -> f54(A,B,C,1 + D,E,F,G) [E >= B] (?,1)
12. f54(A,B,C,D,E,F,G) -> f68(A,B,C,0,E,F,G) [D >= A] (?,1)
13. f46(A,B,C,D,E,F,G) -> f54(A,B,C,0,E,F,G) [D >= A] (?,1)
Signature:
{(f0,7);(f46,7);(f54,7);(f57,7);(f68,7);(f74,7);(f78,7)}
Flow Graph:
[0->{1,2,3,13},1->{1,2,3,13},2->{1,2,3,13},3->{1,2,3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9}
,9->{},10->{8,9},11->{4,12},12->{6,7,10},13->{4,12}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [F,G] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
2. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && C >= 1 + D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
6. f68(A,B,C,D,E) -> f74(A,B,C,D,E) [B >= 1 + D] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
9. f78(A,B,C,D,E) -> f74(A,B,C,D,E) [D >= A] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (?,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1,2,3,13},1->{1,2,3,13},2->{1,2,3,13},3->{1,2,3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9}
,9->{},10->{8,9},11->{4,12},12->{6,7,10},13->{4,12}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, 5, .= 5) (< 0,0,B>, 12, .= 12) (< 0,0,C>, 0, .= 0) (< 0,0,D>, 0, .= 0) (< 0,0,E>, E, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, 1 + C, .+ 1) (< 1,0,E>, E, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, 1 + A + D, .* 1) (< 2,0,E>, E, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, 1 + D, .+ 1) (< 3,0,E>, E, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, 0, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, 1 + E, .+ 1)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, 1 + D, .+ 1) (< 7,0,E>, E, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, 1 + D, .+ 1) (< 8,0,E>, E, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, 0, .= 0) (<10,0,E>, E, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, 1 + D, .+ 1) (<11,0,E>, E, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, 0, .= 0) (<12,0,E>, E, .= 0)
(<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0) (<13,0,D>, 0, .= 0) (<13,0,E>, E, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
2. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && C >= 1 + D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
6. f68(A,B,C,D,E) -> f74(A,B,C,D,E) [B >= 1 + D] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
9. f78(A,B,C,D,E) -> f74(A,B,C,D,E) [D >= A] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (?,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1,2,3,13},1->{1,2,3,13},2->{1,2,3,13},3->{1,2,3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9}
,9->{},10->{8,9},11->{4,12},12->{6,7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 2,0,A>, 5) (< 2,0,B>, 12) (< 2,0,C>, 0) (< 2,0,D>, 5) (< 2,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 6,0,A>, 5) (< 6,0,B>, 12) (< 6,0,C>, 0) (< 6,0,D>, 12) (< 6,0,E>, 12 + E)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(< 9,0,A>, 5) (< 9,0,B>, 12) (< 9,0,C>, 0) (< 9,0,D>, 5) (< 9,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
2. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && C >= 1 + D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
6. f68(A,B,C,D,E) -> f74(A,B,C,D,E) [B >= 1 + D] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
9. f78(A,B,C,D,E) -> f74(A,B,C,D,E) [D >= A] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (?,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1,2,3,13},1->{1,2,3,13},2->{1,2,3,13},3->{1,2,3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9}
,9->{},10->{8,9},11->{4,12},12->{6,7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 2,0,A>, 5) (< 2,0,B>, 12) (< 2,0,C>, 0) (< 2,0,D>, 5) (< 2,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 6,0,A>, 5) (< 6,0,B>, 12) (< 6,0,C>, 0) (< 6,0,D>, 12) (< 6,0,E>, 12 + E)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(< 9,0,A>, 5) (< 9,0,B>, 12) (< 9,0,C>, 0) (< 9,0,D>, 5) (< 9,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,2),(0,3),(0,13),(1,1),(1,2),(2,3),(3,1),(3,2)]
* Step 5: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
2. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && C >= 1 + D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
6. f68(A,B,C,D,E) -> f74(A,B,C,D,E) [B >= 1 + D] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
9. f78(A,B,C,D,E) -> f74(A,B,C,D,E) [D >= A] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (?,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},2->{1,2,13},3->{3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9},9->{},10->{8,9}
,11->{4,12},12->{6,7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 2,0,A>, 5) (< 2,0,B>, 12) (< 2,0,C>, 0) (< 2,0,D>, 5) (< 2,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 6,0,A>, 5) (< 6,0,B>, 12) (< 6,0,C>, 0) (< 6,0,D>, 12) (< 6,0,E>, 12 + E)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(< 9,0,A>, 5) (< 9,0,B>, 12) (< 9,0,C>, 0) (< 9,0,D>, 5) (< 9,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [2]
* Step 6: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
6. f68(A,B,C,D,E) -> f74(A,B,C,D,E) [B >= 1 + D] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
9. f78(A,B,C,D,E) -> f74(A,B,C,D,E) [D >= A] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (?,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},6->{},7->{6,7,10},8->{8,9},9->{},10->{8,9},11->{4,12}
,12->{6,7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 6,0,A>, 5) (< 6,0,B>, 12) (< 6,0,C>, 0) (< 6,0,D>, 12) (< 6,0,E>, 12 + E)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(< 9,0,A>, 5) (< 9,0,B>, 12) (< 9,0,C>, 0) (< 9,0,D>, 5) (< 9,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [6,9]
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (?,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f46) = 1
p(f54) = 0
p(f57) = 0
p(f68) = 0
p(f78) = 0
The following rules are strictly oriented:
[D >= A] ==>
f46(A,B,C,D,E) = 1
> 0
= f54(A,B,C,0,E)
The following rules are weakly oriented:
True ==>
f0(A,B,C,D,E) = 1
>= 1
= f46(5,12,0,0,E)
[A >= 1 + D && C = D] ==>
f46(A,B,C,D,E) = 1
>= 1
= f46(A,B,C,1 + C,E)
[A >= 1 + D && D >= 1 + C] ==>
f46(A,B,C,D,E) = 1
>= 1
= f46(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f54(A,B,C,D,E) = 0
>= 0
= f57(A,B,C,D,0)
[B >= 1 + E] ==>
f57(A,B,C,D,E) = 0
>= 0
= f57(A,B,C,D,1 + E)
[B >= 1 + D] ==>
f68(A,B,C,D,E) = 0
>= 0
= f68(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f78(A,B,C,D,E) = 0
>= 0
= f78(A,B,C,1 + D,E)
[D >= B] ==>
f68(A,B,C,D,E) = 0
>= 0
= f78(A,B,C,0,E)
[E >= B] ==>
f57(A,B,C,D,E) = 0
>= 0
= f54(A,B,C,1 + D,E)
[D >= A] ==>
f54(A,B,C,D,E) = 0
>= 0
= f68(A,B,C,0,E)
* Step 8: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (?,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (?,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f46) = 1
p(f54) = 1
p(f57) = 1
p(f68) = 0
p(f78) = 0
The following rules are strictly oriented:
[D >= A] ==>
f54(A,B,C,D,E) = 1
> 0
= f68(A,B,C,0,E)
The following rules are weakly oriented:
True ==>
f0(A,B,C,D,E) = 1
>= 1
= f46(5,12,0,0,E)
[A >= 1 + D && C = D] ==>
f46(A,B,C,D,E) = 1
>= 1
= f46(A,B,C,1 + C,E)
[A >= 1 + D && D >= 1 + C] ==>
f46(A,B,C,D,E) = 1
>= 1
= f46(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f54(A,B,C,D,E) = 1
>= 1
= f57(A,B,C,D,0)
[B >= 1 + E] ==>
f57(A,B,C,D,E) = 1
>= 1
= f57(A,B,C,D,1 + E)
[B >= 1 + D] ==>
f68(A,B,C,D,E) = 0
>= 0
= f68(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f78(A,B,C,D,E) = 0
>= 0
= f78(A,B,C,1 + D,E)
[D >= B] ==>
f68(A,B,C,D,E) = 0
>= 0
= f78(A,B,C,0,E)
[E >= B] ==>
f57(A,B,C,D,E) = 1
>= 1
= f54(A,B,C,1 + D,E)
[D >= A] ==>
f46(A,B,C,D,E) = 1
>= 1
= f54(A,B,C,0,E)
* Step 10: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (?,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f46) = 1
p(f54) = 1
p(f57) = 1
p(f68) = 1
p(f78) = 0
The following rules are strictly oriented:
[D >= B] ==>
f68(A,B,C,D,E) = 1
> 0
= f78(A,B,C,0,E)
The following rules are weakly oriented:
True ==>
f0(A,B,C,D,E) = 1
>= 1
= f46(5,12,0,0,E)
[A >= 1 + D && C = D] ==>
f46(A,B,C,D,E) = 1
>= 1
= f46(A,B,C,1 + C,E)
[A >= 1 + D && D >= 1 + C] ==>
f46(A,B,C,D,E) = 1
>= 1
= f46(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f54(A,B,C,D,E) = 1
>= 1
= f57(A,B,C,D,0)
[B >= 1 + E] ==>
f57(A,B,C,D,E) = 1
>= 1
= f57(A,B,C,D,1 + E)
[B >= 1 + D] ==>
f68(A,B,C,D,E) = 1
>= 1
= f68(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f78(A,B,C,D,E) = 0
>= 0
= f78(A,B,C,1 + D,E)
[E >= B] ==>
f57(A,B,C,D,E) = 1
>= 1
= f54(A,B,C,1 + D,E)
[D >= A] ==>
f54(A,B,C,D,E) = 1
>= 1
= f68(A,B,C,0,E)
[D >= A] ==>
f46(A,B,C,D,E) = 1
>= 1
= f54(A,B,C,0,E)
* Step 11: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (?,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 5
p(f46) = x1
p(f54) = x1
p(f57) = x1
p(f68) = x1
p(f78) = x1 + -1*x4
The following rules are strictly oriented:
[A >= 1 + D] ==>
f78(A,B,C,D,E) = A + -1*D
> -1 + A + -1*D
= f78(A,B,C,1 + D,E)
The following rules are weakly oriented:
True ==>
f0(A,B,C,D,E) = 5
>= 5
= f46(5,12,0,0,E)
[A >= 1 + D && C = D] ==>
f46(A,B,C,D,E) = A
>= A
= f46(A,B,C,1 + C,E)
[A >= 1 + D && D >= 1 + C] ==>
f46(A,B,C,D,E) = A
>= A
= f46(A,B,C,1 + D,E)
[A >= 1 + D] ==>
f54(A,B,C,D,E) = A
>= A
= f57(A,B,C,D,0)
[B >= 1 + E] ==>
f57(A,B,C,D,E) = A
>= A
= f57(A,B,C,D,1 + E)
[B >= 1 + D] ==>
f68(A,B,C,D,E) = A
>= A
= f68(A,B,C,1 + D,E)
[D >= B] ==>
f68(A,B,C,D,E) = A
>= A
= f78(A,B,C,0,E)
[E >= B] ==>
f57(A,B,C,D,E) = A
>= A
= f54(A,B,C,1 + D,E)
[D >= A] ==>
f54(A,B,C,D,E) = A
>= A
= f68(A,B,C,0,E)
[D >= A] ==>
f46(A,B,C,D,E) = A
>= A
= f54(A,B,C,0,E)
* Step 12: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (?,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (5,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [3], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f46) = x1 + -1*x4
The following rules are strictly oriented:
[A >= 1 + D && D >= 1 + C] ==>
f46(A,B,C,D,E) = A + -1*D
> -1 + A + -1*D
= f46(A,B,C,1 + D,E)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
* Step 13: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (6,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (?,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (5,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [4,11,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f54) = 2 + x1 + -1*x4
p(f57) = 1 + x1 + -1*x4
The following rules are strictly oriented:
[A >= 1 + D] ==>
f54(A,B,C,D,E) = 2 + A + -1*D
> 1 + A + -1*D
= f57(A,B,C,D,0)
The following rules are weakly oriented:
[B >= 1 + E] ==>
f57(A,B,C,D,E) = 1 + A + -1*D
>= 1 + A + -1*D
= f57(A,B,C,D,1 + E)
[E >= B] ==>
f57(A,B,C,D,E) = 1 + A + -1*D
>= 1 + A + -1*D
= f54(A,B,C,1 + D,E)
We use the following global sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
* Step 14: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (6,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (7,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (?,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (5,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f57) = x2 + -1*x5
The following rules are strictly oriented:
[B >= 1 + E] ==>
f57(A,B,C,D,E) = B + -1*E
> -1 + B + -1*E
= f57(A,B,C,D,1 + E)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
* Step 15: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (6,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (7,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (84,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (5,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (?,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 16: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (6,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (7,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (84,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (?,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (5,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (91,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [7], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f68) = x2 + -1*x4
The following rules are strictly oriented:
[B >= 1 + D] ==>
f68(A,B,C,D,E) = B + -1*D
> -1 + B + -1*D
= f68(A,B,C,1 + D,E)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
* Step 17: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f46(5,12,0,0,E) True (1,1)
1. f46(A,B,C,D,E) -> f46(A,B,C,1 + C,E) [A >= 1 + D && C = D] (1,1)
3. f46(A,B,C,D,E) -> f46(A,B,C,1 + D,E) [A >= 1 + D && D >= 1 + C] (6,1)
4. f54(A,B,C,D,E) -> f57(A,B,C,D,0) [A >= 1 + D] (7,1)
5. f57(A,B,C,D,E) -> f57(A,B,C,D,1 + E) [B >= 1 + E] (84,1)
7. f68(A,B,C,D,E) -> f68(A,B,C,1 + D,E) [B >= 1 + D] (12,1)
8. f78(A,B,C,D,E) -> f78(A,B,C,1 + D,E) [A >= 1 + D] (5,1)
10. f68(A,B,C,D,E) -> f78(A,B,C,0,E) [D >= B] (1,1)
11. f57(A,B,C,D,E) -> f54(A,B,C,1 + D,E) [E >= B] (91,1)
12. f54(A,B,C,D,E) -> f68(A,B,C,0,E) [D >= A] (1,1)
13. f46(A,B,C,D,E) -> f54(A,B,C,0,E) [D >= A] (1,1)
Signature:
{(f0,5);(f46,5);(f54,5);(f57,5);(f68,5);(f74,5);(f78,5)}
Flow Graph:
[0->{1},1->{3,13},3->{3,13},4->{5,11},5->{5,11},7->{7,10},8->{8},10->{8},11->{4,12},12->{7,10},13->{4,12}]
Sizebounds:
(< 0,0,A>, 5) (< 0,0,B>, 12) (< 0,0,C>, 0) (< 0,0,D>, 0) (< 0,0,E>, E)
(< 1,0,A>, 5) (< 1,0,B>, 12) (< 1,0,C>, 0) (< 1,0,D>, 1) (< 1,0,E>, E)
(< 3,0,A>, 5) (< 3,0,B>, 12) (< 3,0,C>, 0) (< 3,0,D>, 5) (< 3,0,E>, E)
(< 4,0,A>, 5) (< 4,0,B>, 12) (< 4,0,C>, 0) (< 4,0,D>, 5) (< 4,0,E>, 0)
(< 5,0,A>, 5) (< 5,0,B>, 12) (< 5,0,C>, 0) (< 5,0,D>, 5) (< 5,0,E>, 12)
(< 7,0,A>, 5) (< 7,0,B>, 12) (< 7,0,C>, 0) (< 7,0,D>, 12) (< 7,0,E>, 12 + E)
(< 8,0,A>, 5) (< 8,0,B>, 12) (< 8,0,C>, 0) (< 8,0,D>, 5) (< 8,0,E>, 12 + E)
(<10,0,A>, 5) (<10,0,B>, 12) (<10,0,C>, 0) (<10,0,D>, 0) (<10,0,E>, 12 + E)
(<11,0,A>, 5) (<11,0,B>, 12) (<11,0,C>, 0) (<11,0,D>, 5) (<11,0,E>, 12)
(<12,0,A>, 5) (<12,0,B>, 12) (<12,0,C>, 0) (<12,0,D>, 0) (<12,0,E>, 12 + E)
(<13,0,A>, 5) (<13,0,B>, 12) (<13,0,C>, 0) (<13,0,D>, 0) (<13,0,E>, E)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))