WORST_CASE(?,O(n^1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1)
1. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,C,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,B,S,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [S >= C && A >= D] (?,1)
4. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f29(A,B,C,1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1)
5. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f34(A,B,C,1 + D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1)
6. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f34(A,B,C,1 + D,E,F,G,S,T,J + T,K,L,M,N,O,P,Q,R) [0 >= 1 + S && A >= D] (?,1)
7. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f34(A,B,C,1 + D,E,F,G,S,T,J + T,K,L,M,N,O,P,Q,R) [S >= 1 && A >= D] (?,1)
8. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= K] (?,1)
9. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,1 + D,E,F,G,H,I,S,K,L,M,N,O,P,Q,R) [A >= D] (?,1)
10. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f61(A,B,C,1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1)
11. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f53(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f61(A,B,C,D,E,F,G,H,I,J,K,S,M,N,O,P,Q,R) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,S,T,T,P,Q,R) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,-1*S,T,S,R) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f10(A,1 + B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 && D >= 1 + A] (?,1)
20. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && 0 >= 1 + S] (?,1)
21. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A] (?,1)
Signature:
{(f0,18);(f10,18);(f13,18);(f29,18);(f34,18);(f53,18);(f55,18);(f61,18);(f73,18)}
Flow Graph:
[0->{1,20,21},1->{2,3,17,18,19},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6,7
,14,15},7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{10,11},13->{1,20,21},14->{8,13}
,15->{8,13},16->{5,6,7,14,15},17->{1,20,21},18->{4,16},19->{4,16},20->{},21->{}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [E,F,G,H,I,J,L,M,N,O,P,Q,R] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
4. f29(A,B,C,D,K) -> f29(A,B,C,1 + D,K) [A >= D] (?,1)
5. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [A >= D] (?,1)
6. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [0 >= 1 + S && A >= D] (?,1)
7. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [S >= 1 && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
10. f61(A,B,C,D,K) -> f61(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
20. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A && 0 >= 1 + S] (?,1)
21. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1,20,21},1->{2,3,17,18,19},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6,7
,14,15},7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{10,11},13->{1,20,21},14->{8,13}
,15->{8,13},16->{5,6,7,14,15},17->{1,20,21},18->{4,16},19->{4,16},20->{},21->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,K>, K, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, 0, .= 0) (< 1,0,D>, D, .= 0) (< 1,0,K>, K, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, 1 + D, .+ 1) (< 2,0,K>, K, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, ?, .?) (< 3,0,D>, 1 + D, .+ 1) (< 3,0,K>, K, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, 1 + D, .+ 1) (< 4,0,K>, K, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, 1 + D, .+ 1) (< 5,0,K>, K, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, 1 + D, .+ 1) (< 6,0,K>, K, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, 1 + D, .+ 1) (< 7,0,K>, K, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,K>, K, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, 1 + D, .+ 1) (< 9,0,K>, K, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, 1 + D, .+ 1) (<10,0,K>, K, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,K>, 1 + K, .+ 1)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0) (<12,0,K>, K, .= 0)
(<13,0,A>, A, .= 0) (<13,0,B>, 1 + B, .+ 1) (<13,0,C>, C, .= 0) (<13,0,D>, D, .= 0) (<13,0,K>, K, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0) (<14,0,K>, K, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0) (<15,0,K>, K, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0) (<16,0,K>, K, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, 1 + B, .+ 1) (<17,0,C>, 0, .= 0) (<17,0,D>, D, .= 0) (<17,0,K>, K, .= 0)
(<18,0,A>, A, .= 0) (<18,0,B>, B, .= 0) (<18,0,C>, C, .= 0) (<18,0,D>, D, .= 0) (<18,0,K>, K, .= 0)
(<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, C, .= 0) (<19,0,D>, D, .= 0) (<19,0,K>, K, .= 0)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, C, .= 0) (<20,0,D>, D, .= 0) (<20,0,K>, K, .= 0)
(<21,0,A>, A, .= 0) (<21,0,B>, B, .= 0) (<21,0,C>, C, .= 0) (<21,0,D>, D, .= 0) (<21,0,K>, K, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
4. f29(A,B,C,D,K) -> f29(A,B,C,1 + D,K) [A >= D] (?,1)
5. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [A >= D] (?,1)
6. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [0 >= 1 + S && A >= D] (?,1)
7. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [S >= 1 && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
10. f61(A,B,C,D,K) -> f61(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
20. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A && 0 >= 1 + S] (?,1)
21. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1,20,21},1->{2,3,17,18,19},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6,7
,14,15},7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{10,11},13->{1,20,21},14->{8,13}
,15->{8,13},16->{5,6,7,14,15},17->{1,20,21},18->{4,16},19->{4,16},20->{},21->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,K>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,K>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,K>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,K>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,K>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,K>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,K>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,K>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,K>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) (<20,0,K>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,0,K>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, 1 + A) (< 4,0,K>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, 1 + A) (< 5,0,K>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, 1 + A) (< 6,0,K>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, 1 + A) (< 7,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, 1 + A) (<10,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) (<20,0,K>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,0,K>, ?)
* Step 4: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
4. f29(A,B,C,D,K) -> f29(A,B,C,1 + D,K) [A >= D] (?,1)
5. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [A >= D] (?,1)
6. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [0 >= 1 + S && A >= D] (?,1)
7. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [S >= 1 && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
10. f61(A,B,C,D,K) -> f61(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
20. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A && 0 >= 1 + S] (?,1)
21. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1,20,21},1->{2,3,17,18,19},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6,7
,14,15},7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{10,11},13->{1,20,21},14->{8,13}
,15->{8,13},16->{5,6,7,14,15},17->{1,20,21},18->{4,16},19->{4,16},20->{},21->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, 1 + A) (< 4,0,K>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, 1 + A) (< 5,0,K>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, 1 + A) (< 6,0,K>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, 1 + A) (< 7,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, 1 + A) (<10,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) (<20,0,K>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,0,K>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(1,18)
,(1,19)
,(12,10)
,(16,5)
,(16,6)
,(16,7)
,(18,4)
,(19,4)]
* Step 5: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
4. f29(A,B,C,D,K) -> f29(A,B,C,1 + D,K) [A >= D] (?,1)
5. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [A >= D] (?,1)
6. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [0 >= 1 + S && A >= D] (?,1)
7. f34(A,B,C,D,K) -> f34(A,B,C,1 + D,K) [S >= 1 && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
10. f61(A,B,C,D,K) -> f61(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
20. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A && 0 >= 1 + S] (?,1)
21. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1,20,21},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6,7,14,15}
,7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{11},13->{1,20,21},14->{8,13},15->{8,13}
,16->{14,15},17->{1,20,21},18->{16},19->{16},20->{},21->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, 1 + A) (< 4,0,K>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, 1 + A) (< 5,0,K>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, 1 + A) (< 6,0,K>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, 1 + A) (< 7,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, 1 + A) (<10,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) (<20,0,K>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,0,K>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [4,5,6,7,10]
* Step 6: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
20. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A && 0 >= 1 + S] (?,1)
21. f10(A,B,C,D,K) -> f73(A,B,C,D,K) [B >= A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1,20,21},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11}
,13->{1,20,21},14->{8,13},15->{8,13},16->{14,15},17->{1,20,21},18->{16},19->{16},20->{},21->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) (<20,0,K>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,0,K>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [20,21]
* Step 7: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (?,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 2 + x1 + -1*x2
p(f10) = 2 + x1 + -1*x2
p(f13) = 1 + x1 + -1*x2
p(f29) = 1 + x1 + -1*x2
p(f34) = 1 + x1 + -1*x2
p(f53) = 1 + x1 + -1*x2
p(f55) = 1 + x1 + -1*x2
p(f61) = 1 + x1 + -1*x2
The following rules are strictly oriented:
[A >= 1 + B] ==>
f10(A,B,C,D,K) = 2 + A + -1*B
> 1 + A + -1*B
= f13(A,B,0,D,K)
The following rules are weakly oriented:
[A >= 2] ==>
f0(A,B,C,D,K) = 2 + A + -1*B
>= 2 + A + -1*B
= f10(A,B,C,D,K)
[C >= 1 + S && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f13(A,B,C,1 + D,K)
[S >= C && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f13(A,B,S,1 + D,K)
[A >= K] ==>
f53(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f55(A,B,C,D,K)
[A >= D] ==>
f55(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f55(A,B,C,1 + D,K)
[D >= 1 + A] ==>
f61(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f53(A,B,C,D,1 + K)
[D >= 1 + A] ==>
f55(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f61(A,B,C,D,K)
[K >= 1 + A] ==>
f53(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f10(A,1 + B,C,D,K)
[D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f53(A,B,C,D,K)
[0 >= 1 + U && D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f53(A,B,C,D,K)
[D >= 1 + A] ==>
f29(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f34(A,B,C,D,K)
[D >= 1 + A && C = 0] ==>
f13(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f10(A,1 + B,0,D,K)
[0 >= 1 + C && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f29(A,B,C,D,K)
[C >= 1 && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*B
>= 1 + A + -1*B
= f29(A,B,C,D,K)
* Step 8: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (?,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1 + x1 + -1*x5
p(f10) = 1 + x1 + -1*x5
p(f13) = 1 + x1 + -1*x5
p(f29) = 1 + x1 + -1*x5
p(f34) = 1 + x1 + -1*x5
p(f53) = 1 + x1 + -1*x5
p(f55) = x1 + -1*x5
p(f61) = x1 + -1*x5
The following rules are strictly oriented:
[A >= K] ==>
f53(A,B,C,D,K) = 1 + A + -1*K
> A + -1*K
= f55(A,B,C,D,K)
The following rules are weakly oriented:
[A >= 2] ==>
f0(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f10(A,B,C,D,K)
[A >= 1 + B] ==>
f10(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f13(A,B,0,D,K)
[C >= 1 + S && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f13(A,B,C,1 + D,K)
[S >= C && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f13(A,B,S,1 + D,K)
[A >= D] ==>
f55(A,B,C,D,K) = A + -1*K
>= A + -1*K
= f55(A,B,C,1 + D,K)
[D >= 1 + A] ==>
f61(A,B,C,D,K) = A + -1*K
>= A + -1*K
= f53(A,B,C,D,1 + K)
[D >= 1 + A] ==>
f55(A,B,C,D,K) = A + -1*K
>= A + -1*K
= f61(A,B,C,D,K)
[K >= 1 + A] ==>
f53(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f10(A,1 + B,C,D,K)
[D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f53(A,B,C,D,K)
[0 >= 1 + U && D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f53(A,B,C,D,K)
[D >= 1 + A] ==>
f29(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f34(A,B,C,D,K)
[D >= 1 + A && C = 0] ==>
f13(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f10(A,1 + B,0,D,K)
[0 >= 1 + C && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f29(A,B,C,D,K)
[C >= 1 && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*K
>= 1 + A + -1*K
= f29(A,B,C,D,K)
* Step 9: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (?,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (1 + A + K,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1 + x1 + -1*x4
p(f10) = 1 + x1 + -1*x4
p(f13) = 1 + x1 + -1*x4
p(f29) = 1 + x1 + -1*x4
p(f34) = 1 + x1 + -1*x4
p(f53) = 1 + x1 + -1*x4
p(f55) = 1 + x1 + -1*x4
p(f61) = 1 + x1 + -1*x4
The following rules are strictly oriented:
[S >= C && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
> A + -1*D
= f13(A,B,S,1 + D,K)
The following rules are weakly oriented:
[A >= 2] ==>
f0(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,B,C,D,K)
[A >= 1 + B] ==>
f10(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f13(A,B,0,D,K)
[C >= 1 + S && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= A + -1*D
= f13(A,B,C,1 + D,K)
[A >= K] ==>
f53(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f55(A,B,C,D,K)
[A >= D] ==>
f55(A,B,C,D,K) = 1 + A + -1*D
>= A + -1*D
= f55(A,B,C,1 + D,K)
[D >= 1 + A] ==>
f61(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,1 + K)
[D >= 1 + A] ==>
f55(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f61(A,B,C,D,K)
[K >= 1 + A] ==>
f53(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,1 + B,C,D,K)
[D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,K)
[0 >= 1 + U && D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,K)
[D >= 1 + A] ==>
f29(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f34(A,B,C,D,K)
[D >= 1 + A && C = 0] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,1 + B,0,D,K)
[0 >= 1 + C && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f29(A,B,C,D,K)
[C >= 1 && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f29(A,B,C,D,K)
* Step 10: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (?,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (1 + A + D,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (1 + A + K,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1 + x1 + -1*x4
p(f10) = 1 + x1 + -1*x4
p(f13) = 1 + x1 + -1*x4
p(f29) = 1 + x1 + -1*x4
p(f34) = 1 + x1 + -1*x4
p(f53) = 1 + x1 + -1*x4
p(f55) = 1 + x1 + -1*x4
p(f61) = 1 + x1 + -1*x4
The following rules are strictly oriented:
[C >= 1 + S && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
> A + -1*D
= f13(A,B,C,1 + D,K)
[S >= C && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
> A + -1*D
= f13(A,B,S,1 + D,K)
The following rules are weakly oriented:
[A >= 2] ==>
f0(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,B,C,D,K)
[A >= 1 + B] ==>
f10(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f13(A,B,0,D,K)
[A >= K] ==>
f53(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f55(A,B,C,D,K)
[A >= D] ==>
f55(A,B,C,D,K) = 1 + A + -1*D
>= A + -1*D
= f55(A,B,C,1 + D,K)
[D >= 1 + A] ==>
f61(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,1 + K)
[D >= 1 + A] ==>
f55(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f61(A,B,C,D,K)
[K >= 1 + A] ==>
f53(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,1 + B,C,D,K)
[D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,K)
[0 >= 1 + U && D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,K)
[D >= 1 + A] ==>
f29(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f34(A,B,C,D,K)
[D >= 1 + A && C = 0] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,1 + B,0,D,K)
[0 >= 1 + C && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f29(A,B,C,D,K)
[C >= 1 && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f29(A,B,C,D,K)
* Step 11: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (1 + A + D,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (1 + A + D,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (1 + A + K,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (?,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (?,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (?,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (?,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (?,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (?,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 12: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (1 + A + D,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (1 + A + D,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (1 + A + K,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (?,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (4 + 4*A + 4*D,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (4 + 4*A + 4*D,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (4 + 4*A + 4*D,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (4 + 3*A + B + 2*D,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (2 + 2*A + 2*D,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (2 + 2*A + 2*D,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1 + x1 + -1*x4
p(f10) = 1 + x1 + -1*x4
p(f13) = 1 + x1 + -1*x4
p(f29) = 1 + x1 + -1*x4
p(f34) = 1 + x1 + -1*x4
p(f53) = 1 + x1 + -1*x4
p(f55) = 1 + x1 + -1*x4
p(f61) = 1 + x1 + -1*x4
The following rules are strictly oriented:
[C >= 1 + S && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
> A + -1*D
= f13(A,B,C,1 + D,K)
[S >= C && A >= D] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
> A + -1*D
= f13(A,B,S,1 + D,K)
[A >= D] ==>
f55(A,B,C,D,K) = 1 + A + -1*D
> A + -1*D
= f55(A,B,C,1 + D,K)
The following rules are weakly oriented:
[A >= 2] ==>
f0(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,B,C,D,K)
[A >= 1 + B] ==>
f10(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f13(A,B,0,D,K)
[A >= K] ==>
f53(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f55(A,B,C,D,K)
[D >= 1 + A] ==>
f61(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,1 + K)
[D >= 1 + A] ==>
f55(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f61(A,B,C,D,K)
[K >= 1 + A] ==>
f53(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,1 + B,C,D,K)
[D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,K)
[0 >= 1 + U && D >= 1 + A] ==>
f34(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f53(A,B,C,D,K)
[D >= 1 + A] ==>
f29(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f34(A,B,C,D,K)
[D >= 1 + A && C = 0] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f10(A,1 + B,0,D,K)
[0 >= 1 + C && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f29(A,B,C,D,K)
[C >= 1 && D >= 1 + A] ==>
f13(A,B,C,D,K) = 1 + A + -1*D
>= 1 + A + -1*D
= f29(A,B,C,D,K)
* Step 13: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (1 + A + D,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (1 + A + D,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (1 + A + K,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (1 + A + D,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (?,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (?,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (?,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (4 + 4*A + 4*D,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (4 + 4*A + 4*D,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (4 + 4*A + 4*D,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (4 + 3*A + B + 2*D,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (2 + 2*A + 2*D,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (2 + 2*A + 2*D,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 14: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,K) -> f10(A,B,C,D,K) [A >= 2] (1,1)
1. f10(A,B,C,D,K) -> f13(A,B,0,D,K) [A >= 1 + B] (2 + A + B,1)
2. f13(A,B,C,D,K) -> f13(A,B,C,1 + D,K) [C >= 1 + S && A >= D] (1 + A + D,1)
3. f13(A,B,C,D,K) -> f13(A,B,S,1 + D,K) [S >= C && A >= D] (1 + A + D,1)
8. f53(A,B,C,D,K) -> f55(A,B,C,D,K) [A >= K] (1 + A + K,1)
9. f55(A,B,C,D,K) -> f55(A,B,C,1 + D,K) [A >= D] (1 + A + D,1)
11. f61(A,B,C,D,K) -> f53(A,B,C,D,1 + K) [D >= 1 + A] (2 + 2*A + D + K,1)
12. f55(A,B,C,D,K) -> f61(A,B,C,D,K) [D >= 1 + A] (2 + 2*A + D + K,1)
13. f53(A,B,C,D,K) -> f10(A,1 + B,C,D,K) [K >= 1 + A] (10 + 10*A + 9*D + K,1)
14. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [D >= 1 + A] (4 + 4*A + 4*D,1)
15. f34(A,B,C,D,K) -> f53(A,B,C,D,K) [0 >= 1 + U && D >= 1 + A] (4 + 4*A + 4*D,1)
16. f29(A,B,C,D,K) -> f34(A,B,C,D,K) [D >= 1 + A] (4 + 4*A + 4*D,1)
17. f13(A,B,C,D,K) -> f10(A,1 + B,0,D,K) [D >= 1 + A && C = 0] (4 + 3*A + B + 2*D,1)
18. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [0 >= 1 + C && D >= 1 + A] (2 + 2*A + 2*D,1)
19. f13(A,B,C,D,K) -> f29(A,B,C,D,K) [C >= 1 && D >= 1 + A] (2 + 2*A + 2*D,1)
Signature:
{(f0,5);(f10,5);(f13,5);(f29,5);(f34,5);(f53,5);(f55,5);(f61,5);(f73,5)}
Flow Graph:
[0->{1},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11},13->{1}
,14->{8,13},15->{8,13},16->{14,15},17->{1},18->{16},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,K>, K)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, 0) (< 1,0,D>, ?) (< 1,0,K>, ?)
(< 2,0,A>, A) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, 1 + A) (< 2,0,K>, ?)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, 1 + A) (< 3,0,K>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,K>, A)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, 1 + A) (< 9,0,K>, A)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,K>, A)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,K>, A)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,K>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,K>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,K>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,K>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, 0) (<17,0,D>, ?) (<17,0,K>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,K>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,K>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))