WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1)
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1)
2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (?,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
5. evalrsdbb4in(A,B,C) -> evalrsdreturnin(A,B,C) [A >= 1 + C] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdreturnin(A,B,C) -> evalrsdstop(A,B,C) True (?,1)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[0->{1,2},1->{3},2->{11},3->{4,5},4->{6,7,8},5->{11},6->{9},7->{9},8->{10},9->{4,5},10->{4,5},11->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, 2*A, .?) (< 3,0,C>, 2*A, .?)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, 1 + C, .+ 1)
(<10,0,A>, A, .= 0) (<10,0,B>, 1 + B, .+ 1) (<10,0,C>, 1 + B, .+ 1)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1)
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1)
2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (?,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
5. evalrsdbb4in(A,B,C) -> evalrsdreturnin(A,B,C) [A >= 1 + C] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdreturnin(A,B,C) -> evalrsdstop(A,B,C) True (?,1)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[0->{1,2},1->{3},2->{11},3->{4,5},4->{6,7,8},5->{11},6->{9},7->{9},8->{10},9->{4,5},10->{4,5},11->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?)
* Step 3: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1)
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1)
2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (?,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
5. evalrsdbb4in(A,B,C) -> evalrsdreturnin(A,B,C) [A >= 1 + C] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdreturnin(A,B,C) -> evalrsdstop(A,B,C) True (?,1)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[0->{1,2},1->{3},2->{11},3->{4,5},4->{6,7,8},5->{11},6->{9},7->{9},8->{10},9->{4,5},10->{4,5},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [2,5,11]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1)
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (?,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[0->{1},1->{3},3->{4},4->{6,7,8},6->{9},7->{9},8->{10},9->{4},10->{4}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 1
p(evalrsdbb3in) = 1
p(evalrsdbb4in) = 1
p(evalrsdbbin) = 2
p(evalrsdentryin) = 2
p(evalrsdstart) = 2
The following rules are strictly oriented:
True ==>
evalrsdbbin(A,B,C) = 2
> 1
= evalrsdbb4in(A,2*A,2*A)
The following rules are weakly oriented:
True ==>
evalrsdstart(A,B,C) = 2
>= 2
= evalrsdentryin(A,B,C)
[A >= 0] ==>
evalrsdentryin(A,B,C) = 2
>= 2
= evalrsdbbin(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 1
>= 1
= evalrsdbb1in(A,B,C)
[0 >= 1 + D] ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb2in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb2in(A,B,C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb3in(A,B,C)
True ==>
evalrsdbb2in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb3in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,-1 + B,-1 + B)
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1)
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (2,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[0->{1},1->{3},3->{4},4->{6,7,8},6->{9},7->{9},8->{10},9->{4},10->{4}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1)
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (2,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[0->{1},1->{3},3->{4},4->{6,7,8},6->{9},7->{9},8->{10},9->{4},10->{4}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
ChainProcessor False [0,1,3,4,6,7,8,9,10]
+ Details:
We chained rule 0 to obtain the rules [11] .
* Step 7: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,1)
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (2,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[1->{3},3->{4},4->{6,7,8},6->{9},7->{9},8->{10},9->{4},10->{4},11->{3}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [1]
* Step 8: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) True (2,1)
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[3->{4},4->{6,7,8},6->{9},7->{9},8->{10},9->{4},10->{4},11->{3}]
Sizebounds:
(< 3,0,A>, A) (< 3,0,B>, 2*A) (< 3,0,C>, 2*A)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
+ Applied Processor:
ChainProcessor False [3,4,6,7,8,9,10,11]
+ Details:
We chained rule 3 to obtain the rules [12] .
* Step 9: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [C >= A] (?,1)
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[4->{6,7,8},6->{9},7->{9},8->{10},9->{4},10->{4},11->{12},12->{6,7,8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
+ Applied Processor:
ChainProcessor False [4,6,7,8,9,10,11,12]
+ Details:
We chained rule 4 to obtain the rules [13,14,15] .
* Step 10: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [0 >= 1 + D] (?,1)
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[6->{9},7->{9},8->{10},9->{13,14,15},10->{13,14,15},11->{12},12->{6,7,8},13->{9},14->{9},15->{10}]
Sizebounds:
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
+ Applied Processor:
ChainProcessor False [6,7,8,9,10,11,12,13,14,15]
+ Details:
We chained rule 6 to obtain the rules [16] .
* Step 11: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [D >= 1] (?,1)
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[7->{9},8->{10},9->{13,14,15},10->{13,14,15},11->{12},12->{7,8,16},13->{9},14->{9},15->{10},16->{13,14
,15}]
Sizebounds:
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
+ Applied Processor:
ChainProcessor False [7,8,9,10,11,12,13,14,15,16]
+ Details:
We chained rule 7 to obtain the rules [17] .
* Step 12: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) True (?,1)
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[8->{10},9->{13,14,15},10->{13,14,15},11->{12},12->{8,16,17},13->{9},14->{9},15->{10},16->{13,14,15}
,17->{13,14,15}]
Sizebounds:
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
+ Applied Processor:
ChainProcessor False [8,9,10,11,12,13,14,15,16,17]
+ Details:
We chained rule 8 to obtain the rules [18] .
* Step 13: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) True (?,1)
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[9->{13,14,15},10->{13,14,15},11->{12},12->{16,17,18},13->{9},14->{9},15->{10},16->{13,14,15},17->{13,14
,15},18->{13,14,15}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?)
+ Applied Processor:
ChainProcessor False [9,10,11,12,13,14,15,16,17,18]
+ Details:
We chained rule 9 to obtain the rules [19,20,21] .
* Step 14: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,1)
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[10->{13,14,15},11->{12},12->{16,17,18},13->{19,20,21},14->{19,20,21},15->{10},16->{13,14,15},17->{13,14
,15},18->{13,14,15},19->{19,20,21},20->{19,20,21},21->{10}]
Sizebounds:
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
+ Applied Processor:
ChainProcessor False [10,11,12,13,14,15,16,17,18,19,20,21]
+ Details:
We chained rule 10 to obtain the rules [22,23,24] .
* Step 15: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalrsdstart(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (1,2)
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[11->{12},12->{16,17,18},13->{19,20,21},14->{19,20,21},15->{22,23,24},16->{13,14,15},17->{13,14,15}
,18->{13,14,15},19->{19,20,21},20->{19,20,21},21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24}]
Sizebounds:
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C)
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
+ Applied Processor:
ChainProcessor False [11,12,13,14,15,16,17,18,19,20,21,22,23,24]
+ Details:
We chained rule 11 to obtain the rules [25] .
* Step 16: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
12. evalrsdbbin(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [2*A >= A] (2,2)
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[12->{16,17,18},13->{19,20,21},14->{19,20,21},15->{22,23,24},16->{13,14,15},17->{13,14,15},18->{13,14,15}
,19->{19,20,21},20->{19,20,21},21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{16,17,18}]
Sizebounds:
(<12,0,A>, A) (<12,0,B>, ?) (<12,0,C>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, ?) (<25,0,C>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [12]
* Step 17: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
16. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [0 >= 1 + D] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},16->{13,14,15},17->{13,14,15},18->{13,14,15},19->{19,20,21}
,20->{19,20,21},21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{16,17,18}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, A) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, ?) (<25,0,C>, ?)
+ Applied Processor:
ChainProcessor False [13,14,15,16,17,18,19,20,21,22,23,24,25]
+ Details:
We chained rule 16 to obtain the rules [26,27,28] .
* Step 18: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (?,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (?,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (?,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?)
(<17,0,A>, A) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, A) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, ?) (<25,0,C>, ?)
(<26,0,A>, A) (<26,0,B>, ?) (<26,0,C>, ?)
(<27,0,A>, A) (<27,0,B>, ?) (<27,0,C>, ?)
(<28,0,A>, A) (<28,0,B>, ?) (<28,0,C>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, 1 + C, .+ 1)
(<18,0,A>, A, .= 0) (<18,0,B>, 1 + B, .+ 1) (<18,0,C>, 1 + B, .+ 1)
(<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, 1 + C, .+ 1)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, 1 + C, .+ 1)
(<21,0,A>, A, .= 0) (<21,0,B>, B, .= 0) (<21,0,C>, 1 + C, .+ 1)
(<22,0,A>, A, .= 0) (<22,0,B>, 1 + B, .+ 1) (<22,0,C>, 1 + B, .+ 1)
(<23,0,A>, A, .= 0) (<23,0,B>, 1 + B, .+ 1) (<23,0,C>, 1 + B, .+ 1)
(<24,0,A>, A, .= 0) (<24,0,B>, 1 + B, .+ 1) (<24,0,C>, 1 + B, .+ 1)
(<25,0,A>, A, .= 0) (<25,0,B>, 2*A, .?) (<25,0,C>, 2*A, .?)
(<26,0,A>, A, .= 0) (<26,0,B>, B, .= 0) (<26,0,C>, 1 + C, .+ 1)
(<27,0,A>, A, .= 0) (<27,0,B>, B, .= 0) (<27,0,C>, 1 + C, .+ 1)
(<28,0,A>, A, .= 0) (<28,0,B>, B, .= 0) (<28,0,C>, 1 + C, .+ 1)
* Step 19: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (?,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (?,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (?,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
* Step 20: LocationConstraintsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (?,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (?,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (?,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 13 : True 14 : True 15 : True 17 : [A >= 0] 18 : [A >= 0] 19 : True 20 : True 21 : True 22 : True 23 : True 24 : True 25 : True 26 : [A >= 0] 27 : [A >= 0] 28 : [A >= 0] .
* Step 21: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (?,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (?,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (?,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 0
p(evalrsdstart) = 1
The following rules are strictly oriented:
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb2in(A,B,-1 + C)
* Step 22: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (?,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (?,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 0
p(evalrsdstart) = 1
The following rules are strictly oriented:
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb2in(A,B,-1 + C)
* Step 23: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (?,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 0
p(evalrsdstart) = 1
The following rules are strictly oriented:
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
* Step 24: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (?,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 0
p(evalrsdstart) = 1
The following rules are strictly oriented:
True ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb4in(A,-1 + B,-1 + B)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 0
= evalrsdbb4in(A,B,-1 + C)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
* Step 25: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (?,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 0
p(evalrsdstart) = 1
The following rules are strictly oriented:
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb4in(A,-1 + B,-1 + B)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,C)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
* Step 26: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (?,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 1
p(evalrsdstart) = 1
The following rules are strictly oriented:
[C >= A] ==>
evalrsdbb4in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,C)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 1
>= 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 1
>= 0
= evalrsdbb2in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
* Step 27: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (?,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 1
p(evalrsdstart) = 1
The following rules are strictly oriented:
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,C)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 1
>= 0
= evalrsdbb2in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
* Step 28: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (?,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalrsdbb1in) = 1
p(evalrsdbb2in) = 0
p(evalrsdbb3in) = 0
p(evalrsdbb4in) = 1
p(evalrsdstart) = 1
The following rules are strictly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,C)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[D >= 1] ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = 1
>= 1
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = 1
>= 1
= evalrsdbb1in(A,2*A,2*A)
* Step 29: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (?,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb1in) = -1*x1 + x2
p(evalrsdbb2in) = -1*x1 + x2
p(evalrsdbb3in) = -1*x1 + x2
p(evalrsdbb4in) = -1*x1 + x2
p(evalrsdstart) = x1
The following rules are strictly oriented:
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb3in(A,-1 + B,-1 + B)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1 + -1*A + B
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = -1*A + B
>= -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = -1*A + B
>= -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = A
>= A
= evalrsdbb1in(A,2*A,2*A)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,-1 + C)
* Step 30: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (?,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb1in) = -1*x1 + x2
p(evalrsdbb2in) = -1*x1 + x2
p(evalrsdbb3in) = -1*x1 + x2
p(evalrsdbb4in) = -1*x1 + x2
p(evalrsdstart) = x1
The following rules are strictly oriented:
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb3in(A,-1 + B,-1 + B)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1 + -1*A + B
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = -1*A + B
>= -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = A
>= A
= evalrsdbb1in(A,2*A,2*A)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,-1 + C)
* Step 31: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (?,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (A,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb1in) = -1*x1 + x2
p(evalrsdbb2in) = -1*x1 + x2
p(evalrsdbb3in) = -1*x1 + x2
p(evalrsdbb4in) = -1*x1 + x2
p(evalrsdstart) = x1
The following rules are strictly oriented:
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb3in(A,-1 + B,-1 + B)
The following rules are weakly oriented:
[C >= A && 0 >= 1 + D$] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,C)
[C >= A && D$ >= 1] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,C)
[C >= A] ==>
evalrsdbb4in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,C)
[D >= 1] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb4in(A,B,-1 + C)
True ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1 + -1*A + B
= evalrsdbb4in(A,-1 + B,-1 + B)
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,-1 + C)
[A >= 0 && 2*A >= A] ==>
evalrsdstart(A,B,C) = A
>= A
= evalrsdbb1in(A,2*A,2*A)
[0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A && D$$ >= 1] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb2in(A,B,-1 + C)
[0 >= 1 + D && -1 + C >= A] ==>
evalrsdbb1in(A,B,C) = -1*A + B
>= -1*A + B
= evalrsdbb3in(A,B,-1 + C)
* Step 32: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (A,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (A,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, ?) (<23,0,C>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
* Step 33: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (?,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (A,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (A,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [19,20,21,24], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb2in) = 1
p(evalrsdbb3in) = 0
The following rules are strictly oriented:
[-1 + C >= A] ==>
evalrsdbb2in(A,B,C) = 1
> 0
= evalrsdbb3in(A,B,-1 + C)
The following rules are weakly oriented:
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = 1
>= 1
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = 1
>= 1
= evalrsdbb2in(A,B,-1 + C)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = 0
>= 0
= evalrsdbb3in(A,-1 + B,-1 + B)
We use the following global sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
* Step 34: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (?,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (4 + 2*A,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (A,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (A,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [19,20,22,23,24], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb2in) = -1*x1 + x3
p(evalrsdbb3in) = -1*x1 + x2
The following rules are strictly oriented:
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = -1*A + C
> -1 + -1*A + C
= evalrsdbb2in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb3in(A,-1 + B,-1 + B)
The following rules are weakly oriented:
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = -1*A + C
>= -1 + -1*A + C
= evalrsdbb2in(A,B,-1 + C)
We use the following global sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
* Step 35: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (?,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (9 + 44*A + 12*A^2,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (4 + 2*A,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (A,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (A,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [19,20,22,23,24], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrsdbb2in) = -1*x1 + x3
p(evalrsdbb3in) = -1*x1 + x2
The following rules are strictly oriented:
[-1 + C >= A && 0 >= 1 + D$$] ==>
evalrsdbb2in(A,B,C) = -1*A + C
> -1 + -1*A + C
= evalrsdbb2in(A,B,-1 + C)
[-1 + C >= A && D$$ >= 1] ==>
evalrsdbb2in(A,B,C) = -1*A + C
> -1 + -1*A + C
= evalrsdbb2in(A,B,-1 + C)
[-1 + B >= A && 0 >= 1 + D$$] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A && D$$ >= 1] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb2in(A,-1 + B,-1 + B)
[-1 + B >= A] ==>
evalrsdbb3in(A,B,C) = -1*A + B
> -1 + -1*A + B
= evalrsdbb3in(A,-1 + B,-1 + B)
The following rules are weakly oriented:
We use the following global sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
* Step 36: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && 0 >= 1 + D$] (1,2)
14. evalrsdbb4in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= A && D$ >= 1] (1,2)
15. evalrsdbb4in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= A] (1,2)
17. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [D >= 1] (1,2)
18. evalrsdbb1in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) True (1,2)
19. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && 0 >= 1 + D$$] (9 + 44*A + 12*A^2,3)
20. evalrsdbb2in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [-1 + C >= A && D$$ >= 1] (9 + 44*A + 12*A^2,3)
21. evalrsdbb2in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [-1 + C >= A] (4 + 2*A,3)
22. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && 0 >= 1 + D$$] (A,3)
23. evalrsdbb3in(A,B,C) -> evalrsdbb2in(A,-1 + B,-1 + B) [-1 + B >= A && D$$ >= 1] (A,3)
24. evalrsdbb3in(A,B,C) -> evalrsdbb3in(A,-1 + B,-1 + B) [-1 + B >= A] (A,3)
25. evalrsdstart(A,B,C) -> evalrsdbb1in(A,2*A,2*A) [A >= 0 && 2*A >= A] (1,4)
26. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && 0 >= 1 + D$$] (1,4)
27. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A && D$$ >= 1] (1,4)
28. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,-1 + C) [0 >= 1 + D && -1 + C >= A] (1,4)
Signature:
{(evalrsdbb1in,3)
;(evalrsdbb2in,3)
;(evalrsdbb3in,3)
;(evalrsdbb4in,3)
;(evalrsdbbin,3)
;(evalrsdentryin,3)
;(evalrsdreturnin,3)
;(evalrsdstart,3)
;(evalrsdstop,3)}
Flow Graph:
[13->{19,20,21},14->{19,20,21},15->{22,23,24},17->{13,14,15},18->{13,14,15},19->{19,20,21},20->{19,20,21}
,21->{22,23,24},22->{19,20,21},23->{19,20,21},24->{22,23,24},25->{17,18,26,27,28},26->{19,20,21},27->{19,20
,21},28->{22,23,24}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, 1 + 2*A) (<13,0,C>, 1 + 2*A)
(<14,0,A>, A) (<14,0,B>, 1 + 2*A) (<14,0,C>, 1 + 2*A)
(<15,0,A>, A) (<15,0,B>, 1 + 2*A) (<15,0,C>, 1 + 2*A)
(<17,0,A>, A) (<17,0,B>, 2*A) (<17,0,C>, 1 + 2*A)
(<18,0,A>, A) (<18,0,B>, 1 + 2*A) (<18,0,C>, 1 + 2*A)
(<19,0,A>, A) (<19,0,B>, 1 + 5*A) (<19,0,C>, ?)
(<20,0,A>, A) (<20,0,B>, 1 + 5*A) (<20,0,C>, ?)
(<21,0,A>, A) (<21,0,B>, 1 + 5*A) (<21,0,C>, ?)
(<22,0,A>, A) (<22,0,B>, 1 + 5*A) (<22,0,C>, 2 + 5*A)
(<23,0,A>, A) (<23,0,B>, 1 + 5*A) (<23,0,C>, 2 + 5*A)
(<24,0,A>, A) (<24,0,B>, 1 + 5*A) (<24,0,C>, 2 + 5*A)
(<25,0,A>, A) (<25,0,B>, 2*A) (<25,0,C>, 2*A)
(<26,0,A>, A) (<26,0,B>, 2*A) (<26,0,C>, 1 + 2*A)
(<27,0,A>, A) (<27,0,B>, 2*A) (<27,0,C>, 1 + 2*A)
(<28,0,A>, A) (<28,0,B>, 2*A) (<28,0,C>, 1 + 2*A)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))