WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13,14}
,11->{16,17,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23,24}
,21->{26,27,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0)
(< 1,0,A>, 0, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, D, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, 1 + A, .+ 1) (< 4,0,D>, 3, .= 3)
(< 5,0,A>, 1 + A, .+ 1) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0)
(< 6,0,A>, 1 + A, .+ 1) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0)
(<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0) (<13,0,D>, D, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0)
(<15,0,A>, C, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, C, .= 0) (<17,0,D>, D, .= 0)
(<18,0,A>, A, .= 0) (<18,0,B>, B, .= 0) (<18,0,C>, C, .= 0) (<18,0,D>, D, .= 0)
(<19,0,A>, C, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, C, .= 0) (<19,0,D>, D, .= 0)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, C, .= 0) (<20,0,D>, D, .= 0)
(<21,0,A>, A, .= 0) (<21,0,B>, B, .= 0) (<21,0,C>, C, .= 0) (<21,0,D>, D, .= 0)
(<22,0,A>, A, .= 0) (<22,0,B>, B, .= 0) (<22,0,C>, C, .= 0) (<22,0,D>, D, .= 0)
(<23,0,A>, A, .= 0) (<23,0,B>, B, .= 0) (<23,0,C>, C, .= 0) (<23,0,D>, D, .= 0)
(<24,0,A>, A, .= 0) (<24,0,B>, B, .= 0) (<24,0,C>, C, .= 0) (<24,0,D>, D, .= 0)
(<25,0,A>, C, .= 0) (<25,0,B>, B, .= 0) (<25,0,C>, C, .= 0) (<25,0,D>, D, .= 0)
(<26,0,A>, A, .= 0) (<26,0,B>, B, .= 0) (<26,0,C>, C, .= 0) (<26,0,D>, D, .= 0)
(<27,0,A>, A, .= 0) (<27,0,B>, B, .= 0) (<27,0,C>, C, .= 0) (<27,0,D>, D, .= 0)
(<28,0,A>, A, .= 0) (<28,0,B>, B, .= 0) (<28,0,C>, C, .= 0) (<28,0,D>, D, .= 0)
(<29,0,A>, C, .= 0) (<29,0,B>, B, .= 0) (<29,0,C>, C, .= 0) (<29,0,D>, D, .= 0)
(<30,0,A>, C, .= 0) (<30,0,B>, B, .= 0) (<30,0,C>, C, .= 0) (<30,0,D>, D, .= 0)
(<31,0,A>, A, .= 0) (<31,0,B>, B, .= 0) (<31,0,C>, C, .= 0) (<31,0,D>, D, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13,14}
,11->{16,17,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23,24}
,21->{26,27,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?) (<29,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, B) (<14,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<17,0,A>, B) (<17,0,B>, B) (<17,0,C>, B) (<17,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<24,0,A>, B) (<24,0,B>, B) (<24,0,C>, B) (<24,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<27,0,A>, B) (<27,0,B>, B) (<27,0,C>, B) (<27,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
(<31,0,A>, B) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, 3 + D)
* Step 3: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13,14}
,11->{16,17,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23,24}
,21->{26,27,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, B) (<14,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<17,0,A>, B) (<17,0,B>, B) (<17,0,C>, B) (<17,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<24,0,A>, B) (<24,0,B>, B) (<24,0,C>, B) (<24,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<27,0,A>, B) (<27,0,B>, B) (<27,0,C>, B) (<27,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
(<31,0,A>, B) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, 3 + D)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(10,14),(11,17),(20,24),(21,27)]
* Step 4: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13}
,11->{16,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23},21->{26
,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, B) (<14,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<17,0,A>, B) (<17,0,B>, B) (<17,0,C>, B) (<17,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<24,0,A>, B) (<24,0,B>, B) (<24,0,C>, B) (<24,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<27,0,A>, B) (<27,0,B>, B) (<27,0,C>, B) (<27,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
(<31,0,A>, B) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, 3 + D)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [14,17,24,27]
* Step 5: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13}
,11->{16,18},12->{15},13->{30},15->{2,3},16->{19},18->{30},19->{2,3},20->{22,23},21->{26,28},22->{25}
,23->{30},25->{2,3},26->{29},28->{30},29->{2,3},30->{2,3},31->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
(<31,0,A>, B) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, 3 + D)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3,31]
* Step 6: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2},2->{4,5,6},4->{7},5->{2},6->{2},7->{8,9},8->{10,11},9->{20,21},10->{12,13},11->{16,18}
,12->{15},13->{30},15->{2},16->{19},18->{30},19->{2},20->{22,23},21->{26,28},22->{25},23->{30},25->{2}
,26->{29},28->{30},29->{2},30->{2}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrandom2dLeafBlock1in) = 1
p(evalrandom2dLeafBlock3in) = 1
p(evalrandom2dLeafBlock5in) = 1
p(evalrandom2dLeafBlockin) = 1
p(evalrandom2dNewDefaultin) = 1
p(evalrandom2dNodeBlock7in) = 1
p(evalrandom2dNodeBlock9in) = 1
p(evalrandom2dNodeBlockin) = 1
p(evalrandom2dbb10in) = 1
p(evalrandom2dbb2in) = 1
p(evalrandom2dbb3in) = 1
p(evalrandom2dbb5in) = 1
p(evalrandom2dbb7in) = 1
p(evalrandom2dbb9in) = 1
p(evalrandom2dbbin) = 1
p(evalrandom2dentryin) = 2
p(evalrandom2dstart) = 2
The following rules are strictly oriented:
True ==>
evalrandom2dentryin(A,B,C,D) = 2
> 1
= evalrandom2dbb10in(0,B,C,D)
The following rules are weakly oriented:
True ==>
evalrandom2dstart(A,B,C,D) = 2
>= 2
= evalrandom2dentryin(A,B,C,D)
[B >= 1 + A] ==>
evalrandom2dbb10in(A,B,C,D) = 1
>= 1
= evalrandom2dbbin(A,B,C,D)
[E >= 0 && 3 >= E] ==>
evalrandom2dbbin(A,B,C,D) = 1
>= 1
= evalrandom2dbb2in(A,B,1 + A,E)
[0 >= 1 + E] ==>
evalrandom2dbbin(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(1 + A,B,C,D)
[E >= 4] ==>
evalrandom2dbbin(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(1 + A,B,C,D)
True ==>
evalrandom2dbb2in(A,B,C,D) = 1
>= 1
= evalrandom2dNodeBlock9in(A,B,C,D)
[1 >= D] ==>
evalrandom2dNodeBlock9in(A,B,C,D) = 1
>= 1
= evalrandom2dNodeBlockin(A,B,C,D)
[D >= 2] ==>
evalrandom2dNodeBlock9in(A,B,C,D) = 1
>= 1
= evalrandom2dNodeBlock7in(A,B,C,D)
[0 >= D] ==>
evalrandom2dNodeBlockin(A,B,C,D) = 1
>= 1
= evalrandom2dLeafBlockin(A,B,C,D)
[D >= 1] ==>
evalrandom2dNodeBlockin(A,B,C,D) = 1
>= 1
= evalrandom2dLeafBlock1in(A,B,C,D)
[D = 0] ==>
evalrandom2dLeafBlockin(A,B,C,D) = 1
>= 1
= evalrandom2dbb3in(A,B,C,D)
[0 >= 1 + D] ==>
evalrandom2dLeafBlockin(A,B,C,D) = 1
>= 1
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb3in(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(C,B,C,D)
[D = 1] ==>
evalrandom2dLeafBlock1in(A,B,C,D) = 1
>= 1
= evalrandom2dbb5in(A,B,C,D)
[D >= 2] ==>
evalrandom2dLeafBlock1in(A,B,C,D) = 1
>= 1
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb5in(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(C,B,C,D)
[2 >= D] ==>
evalrandom2dNodeBlock7in(A,B,C,D) = 1
>= 1
= evalrandom2dLeafBlock3in(A,B,C,D)
[D >= 3] ==>
evalrandom2dNodeBlock7in(A,B,C,D) = 1
>= 1
= evalrandom2dLeafBlock5in(A,B,C,D)
[D = 2] ==>
evalrandom2dLeafBlock3in(A,B,C,D) = 1
>= 1
= evalrandom2dbb7in(A,B,C,D)
[1 >= D] ==>
evalrandom2dLeafBlock3in(A,B,C,D) = 1
>= 1
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb7in(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(C,B,C,D)
[D = 3] ==>
evalrandom2dLeafBlock5in(A,B,C,D) = 1
>= 1
= evalrandom2dbb9in(A,B,C,D)
[D >= 4] ==>
evalrandom2dLeafBlock5in(A,B,C,D) = 1
>= 1
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb9in(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(C,B,C,D)
True ==>
evalrandom2dNewDefaultin(A,B,C,D) = 1
>= 1
= evalrandom2dbb10in(C,B,C,D)
* Step 7: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (2,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2},2->{4,5,6},4->{7},5->{2},6->{2},7->{8,9},8->{10,11},9->{20,21},10->{12,13},11->{16,18}
,12->{15},13->{30},15->{2},16->{19},18->{30},19->{2},20->{22,23},21->{26,28},22->{25},23->{30},25->{2}
,26->{29},28->{30},29->{2},30->{2}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrandom2dLeafBlock1in) = x2 + -1*x3
p(evalrandom2dLeafBlock3in) = x2 + -1*x3
p(evalrandom2dLeafBlock5in) = x2 + -1*x3
p(evalrandom2dLeafBlockin) = x2 + -1*x3
p(evalrandom2dNewDefaultin) = x2 + -1*x3
p(evalrandom2dNodeBlock7in) = x2 + -1*x3
p(evalrandom2dNodeBlock9in) = x2 + -1*x3
p(evalrandom2dNodeBlockin) = x2 + -1*x3
p(evalrandom2dbb10in) = -1*x1 + x2
p(evalrandom2dbb2in) = x2 + -1*x3
p(evalrandom2dbb3in) = x2 + -1*x3
p(evalrandom2dbb5in) = x2 + -1*x3
p(evalrandom2dbb7in) = x2 + -1*x3
p(evalrandom2dbb9in) = x2 + -1*x3
p(evalrandom2dbbin) = -1 + -1*x1 + x2
p(evalrandom2dentryin) = x2
p(evalrandom2dstart) = x2
The following rules are strictly oriented:
[B >= 1 + A] ==>
evalrandom2dbb10in(A,B,C,D) = -1*A + B
> -1 + -1*A + B
= evalrandom2dbbin(A,B,C,D)
The following rules are weakly oriented:
True ==>
evalrandom2dstart(A,B,C,D) = B
>= B
= evalrandom2dentryin(A,B,C,D)
True ==>
evalrandom2dentryin(A,B,C,D) = B
>= B
= evalrandom2dbb10in(0,B,C,D)
[E >= 0 && 3 >= E] ==>
evalrandom2dbbin(A,B,C,D) = -1 + -1*A + B
>= -1 + -1*A + B
= evalrandom2dbb2in(A,B,1 + A,E)
[0 >= 1 + E] ==>
evalrandom2dbbin(A,B,C,D) = -1 + -1*A + B
>= -1 + -1*A + B
= evalrandom2dbb10in(1 + A,B,C,D)
[E >= 4] ==>
evalrandom2dbbin(A,B,C,D) = -1 + -1*A + B
>= -1 + -1*A + B
= evalrandom2dbb10in(1 + A,B,C,D)
True ==>
evalrandom2dbb2in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNodeBlock9in(A,B,C,D)
[1 >= D] ==>
evalrandom2dNodeBlock9in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNodeBlockin(A,B,C,D)
[D >= 2] ==>
evalrandom2dNodeBlock9in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNodeBlock7in(A,B,C,D)
[0 >= D] ==>
evalrandom2dNodeBlockin(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dLeafBlockin(A,B,C,D)
[D >= 1] ==>
evalrandom2dNodeBlockin(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dLeafBlock1in(A,B,C,D)
[D = 0] ==>
evalrandom2dLeafBlockin(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb3in(A,B,C,D)
[0 >= 1 + D] ==>
evalrandom2dLeafBlockin(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb3in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb10in(C,B,C,D)
[D = 1] ==>
evalrandom2dLeafBlock1in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb5in(A,B,C,D)
[D >= 2] ==>
evalrandom2dLeafBlock1in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb5in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb10in(C,B,C,D)
[2 >= D] ==>
evalrandom2dNodeBlock7in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dLeafBlock3in(A,B,C,D)
[D >= 3] ==>
evalrandom2dNodeBlock7in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dLeafBlock5in(A,B,C,D)
[D = 2] ==>
evalrandom2dLeafBlock3in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb7in(A,B,C,D)
[1 >= D] ==>
evalrandom2dLeafBlock3in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb7in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb10in(C,B,C,D)
[D = 3] ==>
evalrandom2dLeafBlock5in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb9in(A,B,C,D)
[D >= 4] ==>
evalrandom2dLeafBlock5in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dNewDefaultin(A,B,C,D)
True ==>
evalrandom2dbb9in(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb10in(C,B,C,D)
True ==>
evalrandom2dNewDefaultin(A,B,C,D) = B + -1*C
>= B + -1*C
= evalrandom2dbb10in(C,B,C,D)
* Step 8: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (2,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (B,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2},2->{4,5,6},4->{7},5->{2},6->{2},7->{8,9},8->{10,11},9->{20,21},10->{12,13},11->{16,18}
,12->{15},13->{30},15->{2},16->{19},18->{30},19->{2},20->{22,23},21->{26,28},22->{25},23->{30},25->{2}
,26->{29},28->{30},29->{2},30->{2}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1)
1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (2,1)
2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (B,1)
4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (B,1)
5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (B,1)
6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (B,1)
7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (B,1)
8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (B,1)
9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (B,1)
10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (B,1)
11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (B,1)
12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (B,1)
13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (B,1)
15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1)
16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (B,1)
18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (B,1)
19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1)
20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (B,1)
21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (B,1)
22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (B,1)
23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (B,1)
25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1)
26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (B,1)
28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (B,1)
29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1)
30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (4*B,1)
Signature:
{(evalrandom2dLeafBlock1in,4)
;(evalrandom2dLeafBlock3in,4)
;(evalrandom2dLeafBlock5in,4)
;(evalrandom2dLeafBlockin,4)
;(evalrandom2dNewDefaultin,4)
;(evalrandom2dNodeBlock7in,4)
;(evalrandom2dNodeBlock9in,4)
;(evalrandom2dNodeBlockin,4)
;(evalrandom2dbb10in,4)
;(evalrandom2dbb2in,4)
;(evalrandom2dbb3in,4)
;(evalrandom2dbb5in,4)
;(evalrandom2dbb7in,4)
;(evalrandom2dbb9in,4)
;(evalrandom2dbbin,4)
;(evalrandom2dentryin,4)
;(evalrandom2dreturnin,4)
;(evalrandom2dstart,4)
;(evalrandom2dstop,4)}
Flow Graph:
[0->{1},1->{2},2->{4,5,6},4->{7},5->{2},6->{2},7->{8,9},8->{10,11},9->{20,21},10->{12,13},11->{16,18}
,12->{15},13->{30},15->{2},16->{19},18->{30},19->{2},20->{22,23},21->{26,28},22->{25},23->{30},25->{2}
,26->{29},28->{30},29->{2},30->{2}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 0) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, ?) (< 2,0,D>, 3 + D)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, B) (< 4,0,D>, 3)
(< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, 3 + D)
(< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, 3 + D)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, B) (< 7,0,D>, 3)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, B) (< 8,0,D>, 3)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, B) (< 9,0,D>, 3)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, B) (<10,0,D>, 3)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, B) (<11,0,D>, 3)
(<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, B) (<12,0,D>, 3)
(<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, B) (<13,0,D>, 3)
(<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, B) (<15,0,D>, 3)
(<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, B) (<16,0,D>, 3)
(<18,0,A>, B) (<18,0,B>, B) (<18,0,C>, B) (<18,0,D>, 3)
(<19,0,A>, B) (<19,0,B>, B) (<19,0,C>, B) (<19,0,D>, 3)
(<20,0,A>, B) (<20,0,B>, B) (<20,0,C>, B) (<20,0,D>, 3)
(<21,0,A>, B) (<21,0,B>, B) (<21,0,C>, B) (<21,0,D>, 3)
(<22,0,A>, B) (<22,0,B>, B) (<22,0,C>, B) (<22,0,D>, 3)
(<23,0,A>, B) (<23,0,B>, B) (<23,0,C>, B) (<23,0,D>, 3)
(<25,0,A>, B) (<25,0,B>, B) (<25,0,C>, B) (<25,0,D>, 3)
(<26,0,A>, B) (<26,0,B>, B) (<26,0,C>, B) (<26,0,D>, 3)
(<28,0,A>, B) (<28,0,B>, B) (<28,0,C>, B) (<28,0,D>, 3)
(<29,0,A>, B) (<29,0,B>, B) (<29,0,C>, B) (<29,0,D>, 3)
(<30,0,A>, B) (<30,0,B>, B) (<30,0,C>, B) (<30,0,D>, 3)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))