WORST_CASE(?,O(n^3))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1)
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (?,1)
2. evalfbb3in(A,B,C,D) -> evalfreturnin(A,B,C,D) [D >= B] (?,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
6. evalfbb4in(A,B,C,D) -> evalfreturnin(A,B,C,D) True (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, 0, .= 0) (< 1,0,D>, 0, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, 1 + C, .+ 1) (< 9,0,D>, D, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, 0, .= 0) (<10,0,D>, 1 + D, .+ 1)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1)
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (?,1)
2. evalfbb3in(A,B,C,D) -> evalfreturnin(A,B,C,D) [D >= B] (?,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
6. evalfbb4in(A,B,C,D) -> evalfreturnin(A,B,C,D) True (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, 0) (< 1,0,D>, 0)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, A) (< 2,0,D>, B)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, A) (< 6,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, A) (<11,0,D>, B)
* Step 3: UnsatPaths WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1)
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (?,1)
2. evalfbb3in(A,B,C,D) -> evalfreturnin(A,B,C,D) [D >= B] (?,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
6. evalfbb4in(A,B,C,D) -> evalfreturnin(A,B,C,D) True (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, 0) (< 1,0,D>, 0)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, A) (< 2,0,D>, B)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, A) (< 6,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, A) (<11,0,D>, B)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(1,2)]
* Step 4: LeafRules WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1)
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (?,1)
2. evalfbb3in(A,B,C,D) -> evalfreturnin(A,B,C,D) [D >= B] (?,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
6. evalfbb4in(A,B,C,D) -> evalfreturnin(A,B,C,D) True (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[0->{1},1->{3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, 0) (< 1,0,D>, 0)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, A) (< 2,0,D>, B)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, A) (< 6,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, A) (<11,0,D>, B)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [2,6,11]
* Step 5: PolyRank WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1)
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (?,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[0->{1},1->{3},3->{4,5},4->{7,8},5->{7,8},7->{9},8->{10},9->{3},10->{3}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, 0) (< 1,0,D>, 0)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalfbb1in) = 1
p(evalfbb2in) = 1
p(evalfbb3in) = 1
p(evalfbb4in) = 1
p(evalfbbin) = 1
p(evalfentryin) = 2
p(evalfstart) = 2
The following rules are strictly oriented:
[A >= 1 && B >= 1 + A] ==>
evalfentryin(A,B,C,D) = 2
> 1
= evalfbb3in(A,B,0,0)
The following rules are weakly oriented:
True ==>
evalfstart(A,B,C,D) = 2
>= 2
= evalfentryin(A,B,C,D)
[B >= 1 + D] ==>
evalfbb3in(A,B,C,D) = 1
>= 1
= evalfbb4in(A,B,C,D)
[0 >= 1 + E] ==>
evalfbb4in(A,B,C,D) = 1
>= 1
= evalfbbin(A,B,C,D)
[E >= 1] ==>
evalfbb4in(A,B,C,D) = 1
>= 1
= evalfbbin(A,B,C,D)
[A >= 1 + C] ==>
evalfbbin(A,B,C,D) = 1
>= 1
= evalfbb1in(A,B,C,D)
[C >= A] ==>
evalfbbin(A,B,C,D) = 1
>= 1
= evalfbb2in(A,B,C,D)
True ==>
evalfbb1in(A,B,C,D) = 1
>= 1
= evalfbb3in(A,B,1 + C,D)
True ==>
evalfbb2in(A,B,C,D) = 1
>= 1
= evalfbb3in(A,B,0,1 + D)
* Step 6: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1)
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (2,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[0->{1},1->{3},3->{4,5},4->{7,8},5->{7,8},7->{9},8->{10},9->{3},10->{3}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, 0) (< 1,0,D>, 0)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
+ Applied Processor:
ChainProcessor False [0,1,3,4,5,7,8,9,10]
+ Details:
We chained rule 0 to obtain the rules [11] .
* Step 7: UnreachableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
1. evalfentryin(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (2,1)
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[1->{3},3->{4,5},4->{7,8},5->{7,8},7->{9},8->{10},9->{3},10->{3},11->{3}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, 0) (< 1,0,D>, 0)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
+ 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^3))
+ Considered Problem:
Rules:
3. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [B >= 1 + D] (?,1)
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[3->{4,5},4->{7,8},5->{7,8},7->{9},8->{10},9->{3},10->{3},11->{3}]
Sizebounds:
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, A) (< 3,0,D>, B)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
+ Applied Processor:
ChainProcessor False [3,4,5,7,8,9,10,11]
+ Details:
We chained rule 3 to obtain the rules [12,13] .
* Step 9: UnreachableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
4. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [0 >= 1 + E] (?,1)
5. evalfbb4in(A,B,C,D) -> evalfbbin(A,B,C,D) [E >= 1] (?,1)
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[4->{7,8},5->{7,8},7->{9},8->{10},9->{12,13},10->{12,13},11->{12,13},12->{7,8},13->{7,8}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, A) (< 4,0,D>, B)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, A) (< 5,0,D>, B)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [4,5]
* Step 10: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
7. evalfbbin(A,B,C,D) -> evalfbb1in(A,B,C,D) [A >= 1 + C] (?,1)
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[7->{9},8->{10},9->{12,13},10->{12,13},11->{12,13},12->{7,8},13->{7,8}]
Sizebounds:
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, A) (< 7,0,D>, B)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
+ Applied Processor:
ChainProcessor False [7,8,9,10,11,12,13]
+ Details:
We chained rule 7 to obtain the rules [14] .
* Step 11: UnreachableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
9. evalfbb1in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) True (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[8->{10},9->{12,13},10->{12,13},11->{12,13},12->{8,14},13->{8,14},14->{12,13}]
Sizebounds:
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, A) (< 9,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [9]
* Step 12: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
8. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= A] (?,1)
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[8->{10},10->{12,13},11->{12,13},12->{8,14},13->{8,14},14->{12,13}]
Sizebounds:
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, A) (< 8,0,D>, B)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
+ Applied Processor:
ChainProcessor False [8,10,11,12,13,14]
+ Details:
We chained rule 8 to obtain the rules [15] .
* Step 13: UnreachableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) True (?,1)
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[10->{12,13},11->{12,13},12->{14,15},13->{14,15},14->{12,13},15->{12,13}]
Sizebounds:
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, 0) (<10,0,D>, B)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [10]
* Step 14: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
11. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,0) [A >= 1 && B >= 1 + A] (1,2)
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[11->{12,13},12->{14,15},13->{14,15},14->{12,13},15->{12,13}]
Sizebounds:
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, 0) (<11,0,D>, 0)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
+ Applied Processor:
ChainProcessor False [11,12,13,14,15]
+ Details:
We chained rule 11 to obtain the rules [16,17] .
* Step 15: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
12. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && 0 >= 1 + E$] (?,2)
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
16. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$] (1,4)
17. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1] (1,4)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[12->{14,15},13->{14,15},14->{12,13},15->{12,13},16->{14,15},17->{14,15}]
Sizebounds:
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, A) (<12,0,D>, B)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
(<16,0,A>, A) (<16,0,B>, B) (<16,0,C>, A) (<16,0,D>, B)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, A) (<17,0,D>, B)
+ Applied Processor:
ChainProcessor False [12,13,14,15,16,17]
+ Details:
We chained rule 12 to obtain the rules [18,19] .
* Step 16: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
13. evalfbb3in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 1 + D && E$ >= 1] (?,2)
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
16. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$] (1,4)
17. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1] (1,4)
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[13->{14,15},14->{13,18,19},15->{13,18,19},16->{14,15},17->{14,15},18->{13,18,19},19->{13,18,19}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, A) (<13,0,D>, B)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
(<16,0,A>, A) (<16,0,B>, B) (<16,0,C>, A) (<16,0,D>, B)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, A) (<17,0,D>, B)
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
+ Applied Processor:
ChainProcessor False [13,14,15,16,17,18,19]
+ Details:
We chained rule 13 to obtain the rules [20,21] .
* Step 17: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
16. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$] (1,4)
17. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1] (1,4)
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[14->{18,19,20,21},15->{18,19,20,21},16->{14,15},17->{14,15},18->{18,19,20,21},19->{18,19,20,21},20->{18
,19,20,21},21->{18,19,20,21}]
Sizebounds:
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
(<16,0,A>, A) (<16,0,B>, B) (<16,0,C>, A) (<16,0,D>, B)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, A) (<17,0,D>, B)
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
+ Applied Processor:
ChainProcessor False [14,15,16,17,18,19,20,21]
+ Details:
We chained rule 16 to obtain the rules [22,23] .
* Step 18: ChainProcessor WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
17. evalfstart(A,B,C,D) -> evalfbbin(A,B,0,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1] (1,4)
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[14->{18,19,20,21},15->{18,19,20,21},17->{14,15},18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21}
,21->{18,19,20,21},22->{18,19,20,21},23->{18,19,20,21}]
Sizebounds:
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, A) (<17,0,D>, B)
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, A) (<22,0,D>, B)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, B)
+ Applied Processor:
ChainProcessor False [14,15,17,18,19,20,21,22,23]
+ Details:
We chained rule 17 to obtain the rules [24,25] .
* Step 19: UnreachableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
14. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [A >= 1 + C] (?,2)
15. evalfbbin(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [C >= A] (?,2)
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[14->{18,19,20,21},15->{18,19,20,21},18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20
,21},22->{18,19,20,21},23->{18,19,20,21},24->{18,19,20,21},25->{18,19,20,21}]
Sizebounds:
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, A) (<14,0,D>, B)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, 0) (<15,0,D>, B)
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, A) (<22,0,D>, B)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, B)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, A) (<24,0,D>, B)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, B)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [14,15]
* Step 20: UnsatPaths WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{18,19,20
,21},24->{18,19,20,21},25->{18,19,20,21}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, A) (<22,0,D>, B)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, B)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, A) (<24,0,D>, B)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, B)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(23,18)
,(23,19)
,(23,20)
,(23,21)
,(25,18)
,(25,19)
,(25,20)
,(25,21)]
* Step 21: LocalSizeboundsProc WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, A) (<22,0,D>, B)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, B)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, A) (<24,0,D>, B)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, B)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<18,0,A>, A, .= 0) (<18,0,B>, B, .= 0) (<18,0,C>, 1 + C, .+ 1) (<18,0,D>, D, .= 0)
(<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, 0, .= 0) (<19,0,D>, 1 + D, .+ 1)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, 1 + C, .+ 1) (<20,0,D>, D, .= 0)
(<21,0,A>, A, .= 0) (<21,0,B>, B, .= 0) (<21,0,C>, 0, .= 0) (<21,0,D>, 1 + D, .+ 1)
(<22,0,A>, A, .= 0) (<22,0,B>, B, .= 0) (<22,0,C>, 1, .= 1) (<22,0,D>, 0, .= 0)
(<23,0,A>, A, .= 0) (<23,0,B>, B, .= 0) (<23,0,C>, 0, .= 0) (<23,0,D>, 1, .= 1)
(<24,0,A>, A, .= 0) (<24,0,B>, B, .= 0) (<24,0,C>, 1, .= 1) (<24,0,D>, 0, .= 0)
(<25,0,A>, A, .= 0) (<25,0,B>, B, .= 0) (<25,0,C>, 0, .= 0) (<25,0,D>, 1, .= 1)
* Step 22: SizeboundsProc WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
* Step 23: LocationConstraintsProc WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 18 : [E$$ >= 1] 19 : [E$$ >= 1] 20 : [E$$ >= 1] 21 : [E$$ >= 1] 22 : True 23 : True 24 : True 25 : True .
* Step 24: PolyRank WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (?,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalfbb3in) = x2 + -1*x4
p(evalfstart) = x2
The following rules are strictly oriented:
[B >= 1 + D && E$ >= 1 && C >= A] ==>
evalfbb3in(A,B,C,D) = B + -1*D
> -1 + B + -1*D
= evalfbb3in(A,B,0,1 + D)
[A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] ==>
evalfstart(A,B,C,D) = B
> -1 + B
= evalfbb3in(A,B,0,1)
[A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] ==>
evalfstart(A,B,C,D) = B
> -1 + B
= evalfbb3in(A,B,0,1)
The following rules are weakly oriented:
[B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = B + -1*D
>= B + -1*D
= evalfbb3in(A,B,1 + C,D)
[B >= 1 + D && 0 >= 1 + E$ && C >= A] ==>
evalfbb3in(A,B,C,D) = B + -1*D
>= -1 + B + -1*D
= evalfbb3in(A,B,0,1 + D)
[B >= 1 + D && E$ >= 1 && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = B + -1*D
>= B + -1*D
= evalfbb3in(A,B,1 + C,D)
[A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] ==>
evalfstart(A,B,C,D) = B
>= B
= evalfbb3in(A,B,1,0)
[A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] ==>
evalfstart(A,B,C,D) = B
>= B
= evalfbb3in(A,B,1,0)
* Step 25: PolyRank WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (?,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (B,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalfbb3in) = x2 + -1*x4
p(evalfstart) = x2
The following rules are strictly oriented:
[B >= 1 + D && 0 >= 1 + E$ && C >= A] ==>
evalfbb3in(A,B,C,D) = B + -1*D
> -1 + B + -1*D
= evalfbb3in(A,B,0,1 + D)
[B >= 1 + D && E$ >= 1 && C >= A] ==>
evalfbb3in(A,B,C,D) = B + -1*D
> -1 + B + -1*D
= evalfbb3in(A,B,0,1 + D)
[A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] ==>
evalfstart(A,B,C,D) = B
> -1 + B
= evalfbb3in(A,B,0,1)
[A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] ==>
evalfstart(A,B,C,D) = B
> -1 + B
= evalfbb3in(A,B,0,1)
The following rules are weakly oriented:
[B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = B + -1*D
>= B + -1*D
= evalfbb3in(A,B,1 + C,D)
[B >= 1 + D && E$ >= 1 && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = B + -1*D
>= B + -1*D
= evalfbb3in(A,B,1 + C,D)
[A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] ==>
evalfstart(A,B,C,D) = B
>= B
= evalfbb3in(A,B,1,0)
[A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] ==>
evalfstart(A,B,C,D) = B
>= B
= evalfbb3in(A,B,1,0)
* Step 26: PolyRank WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (B,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (?,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (B,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [18,20], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalfbb3in) = x1 + -1*x3
The following rules are strictly oriented:
[B >= 1 + D && E$ >= 1 && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = A + -1*C
> -1 + A + -1*C
= evalfbb3in(A,B,1 + C,D)
The following rules are weakly oriented:
[B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = A + -1*C
>= -1 + A + -1*C
= evalfbb3in(A,B,1 + C,D)
We use the following global sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
* Step 27: PolyRank WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (?,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (B,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (2 + 2*A + 2*A*B,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (B,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [18], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalfbb3in) = x1 + -1*x3
The following rules are strictly oriented:
[B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] ==>
evalfbb3in(A,B,C,D) = A + -1*C
> -1 + A + -1*C
= evalfbb3in(A,B,1 + C,D)
The following rules are weakly oriented:
We use the following global sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
* Step 28: KnowledgePropagation WORST_CASE(?,O(n^3))
+ Considered Problem:
Rules:
18. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && 0 >= 1 + E$ && A >= 1 + C] (2 + 6*A + 2*A*B + 4*A^2 + 4*A^2*B,4)
19. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && 0 >= 1 + E$ && C >= A] (B,4)
20. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,1 + C,D) [B >= 1 + D && E$ >= 1 && A >= 1 + C] (2 + 2*A + 2*A*B,4)
21. evalfbb3in(A,B,C,D) -> evalfbb3in(A,B,0,1 + D) [B >= 1 + D && E$ >= 1 && C >= A] (B,4)
22. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && A >= 1] (1,6)
23. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && 0 >= 1 + E$$ && 0 >= A] (1,6)
24. evalfstart(A,B,C,D) -> evalfbb3in(A,B,1,0) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && A >= 1] (1,6)
25. evalfstart(A,B,C,D) -> evalfbb3in(A,B,0,1) [A >= 1 && B >= 1 + A && B >= 1 && E$$ >= 1 && 0 >= A] (1,6)
Signature:
{(evalfbb1in,4)
;(evalfbb2in,4)
;(evalfbb3in,4)
;(evalfbb4in,4)
;(evalfbbin,4)
;(evalfentryin,4)
;(evalfreturnin,4)
;(evalfstart,4)
;(evalfstop,4)}
Flow Graph:
[18->{18,19,20,21},19->{18,19,20,21},20->{18,19,20,21},21->{18,19,20,21},22->{18,19,20,21},23->{},24->{18
,19,20,21},25->{}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, B) (<18,0,C>, A) (<18,0,D>, B)
(<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, 0) (<19,0,D>, B)
(<20,0,A>, A) (<20,0,B>, B) (<20,0,C>, A) (<20,0,D>, B)
(<21,0,A>, A) (<21,0,B>, B) (<21,0,C>, 0) (<21,0,D>, B)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, 1) (<22,0,D>, 0)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, 0) (<23,0,D>, 1)
(<24,0,A>, A) (<24,0,B>, B) (<24,0,C>, 1) (<24,0,D>, 0)
(<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, 0) (<25,0,D>, 1)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^3))