WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1)
1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1)
2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1)
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [2 + A >= B && 2 + B >= A] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6}
,11->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0)
(< 3,0,A>, B, .= 0) (< 3,0,B>, A, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1)
(<10,0,A>, 1 + A, .+ 1) (<10,0,B>, B, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1)
1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1)
2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1)
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [2 + A >= B && 2 + B >= A] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6}
,11->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, ?) (<11,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, A) (< 1,0,B>, B)
(< 2,0,A>, A) (< 2,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, A)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, ?) (<11,0,B>, ?)
* Step 3: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1)
1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1)
2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1)
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [2 + A >= B && 2 + B >= A] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6}
,11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, A) (< 1,0,B>, B)
(< 2,0,A>, A) (< 2,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, A)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, ?) (<11,0,B>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(4,7),(5,8)]
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1)
1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1)
2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1)
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [2 + A >= B && 2 + B >= A] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{8},5->{7},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, A) (< 1,0,B>, B)
(< 2,0,A>, A) (< 2,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, A)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, ?) (<11,0,B>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [1,2,6,11]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1)
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[0->{3},3->{4,5},4->{8},5->{7},7->{9},8->{10},9->{4,5},10->{4,5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, A)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwisebb3in) = 0
p(evalwisebb4in) = 0
p(evalwisebb5in) = 0
p(evalwisebb6in) = 0
p(evalwiseentryin) = 1 + x1
p(evalwisestart) = 1 + x1
The following rules are strictly oriented:
[A >= 0 && B >= 0] ==>
evalwiseentryin(A,B) = 1 + A
> 0
= evalwisebb6in(B,A)
The following rules are weakly oriented:
True ==>
evalwisestart(A,B) = 1 + A
>= 1 + A
= evalwiseentryin(A,B)
[B >= 3 + A] ==>
evalwisebb6in(A,B) = 0
>= 0
= evalwisebb3in(A,B)
[A >= 3 + B] ==>
evalwisebb6in(A,B) = 0
>= 0
= evalwisebb3in(A,B)
[A >= 1 + B] ==>
evalwisebb3in(A,B) = 0
>= 0
= evalwisebb4in(A,B)
[B >= A] ==>
evalwisebb3in(A,B) = 0
>= 0
= evalwisebb5in(A,B)
True ==>
evalwisebb4in(A,B) = 0
>= 0
= evalwisebb6in(A,1 + B)
True ==>
evalwisebb5in(A,B) = 0
>= 0
= evalwisebb6in(1 + A,B)
* Step 6: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1)
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1 + A,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[0->{3},3->{4,5},4->{8},5->{7},7->{9},8->{10},9->{4,5},10->{4,5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, A)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
+ Applied Processor:
ChainProcessor False [0,3,4,5,7,8,9,10]
+ Details:
We chained rule 0 to obtain the rules [11] .
* Step 7: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1 + A,1)
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[3->{4,5},4->{7,8},5->{7,8},7->{9},8->{10},9->{4,5},10->{4,5},11->{4,5}]
Sizebounds:
(< 3,0,A>, B) (< 3,0,B>, A)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, B) (<11,0,B>, A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [3]
* Step 8: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 3 + A] (?,1)
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[4->{7,8},5->{7,8},7->{9},8->{10},9->{4,5},10->{4,5},11->{4,5}]
Sizebounds:
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, B) (<11,0,B>, A)
+ Applied Processor:
ChainProcessor False [4,5,7,8,9,10,11]
+ Details:
We chained rule 4 to obtain the rules [12,13] .
* Step 9: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [A >= 3 + B] (?,1)
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
12. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [B >= 3 + A && A >= 1 + B] (?,2)
13. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [B >= 3 + A && B >= A] (?,2)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[5->{7,8},7->{9},8->{10},9->{5,12,13},10->{5,12,13},11->{5,12,13},12->{9},13->{10}]
Sizebounds:
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, B) (<11,0,B>, A)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
+ Applied Processor:
ChainProcessor False [5,7,8,9,10,11,12,13]
+ Details:
We chained rule 5 to obtain the rules [14,15] .
* Step 10: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [A >= 1 + B] (?,1)
8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= A] (?,1)
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
12. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [B >= 3 + A && A >= 1 + B] (?,2)
13. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [B >= 3 + A && B >= A] (?,2)
14. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [A >= 3 + B && A >= 1 + B] (?,2)
15. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [A >= 3 + B && B >= A] (?,2)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[7->{9},8->{10},9->{12,13,14,15},10->{12,13,14,15},11->{12,13,14,15},12->{9},13->{10},14->{9},15->{10}]
Sizebounds:
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, B) (<11,0,B>, A)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [7,8]
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) True (?,1)
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
12. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [B >= 3 + A && A >= 1 + B] (?,2)
13. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [B >= 3 + A && B >= A] (?,2)
14. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [A >= 3 + B && A >= 1 + B] (?,2)
15. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [A >= 3 + B && B >= A] (?,2)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[9->{12,13,14,15},10->{12,13,14,15},11->{12,13,14,15},12->{9},13->{10},14->{9},15->{10}]
Sizebounds:
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, B) (<11,0,B>, A)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
+ Applied Processor:
ChainProcessor False [9,10,11,12,13,14,15]
+ Details:
We chained rule 9 to obtain the rules [16,17,18,19] .
* Step 12: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) True (?,1)
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
12. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [B >= 3 + A && A >= 1 + B] (?,2)
13. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [B >= 3 + A && B >= A] (?,2)
14. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [A >= 3 + B && A >= 1 + B] (?,2)
15. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [A >= 3 + B && B >= A] (?,2)
16. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [1 + B >= 3 + A && A >= 2 + B] (?,3)
17. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [1 + B >= 3 + A && 1 + B >= A] (?,3)
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
19. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [A >= 4 + B && 1 + B >= A] (?,3)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[10->{12,13,14,15},11->{12,13,14,15},12->{16,17,18,19},13->{10},14->{16,17,18,19},15->{10},16->{16,17,18
,19},17->{10},18->{16,17,18,19},19->{10}]
Sizebounds:
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, B) (<11,0,B>, A)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
+ Applied Processor:
ChainProcessor False [10,11,12,13,14,15,16,17,18,19]
+ Details:
We chained rule 10 to obtain the rules [20,21,22,23] .
* Step 13: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. evalwisestart(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,2)
12. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [B >= 3 + A && A >= 1 + B] (?,2)
13. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [B >= 3 + A && B >= A] (?,2)
14. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [A >= 3 + B && A >= 1 + B] (?,2)
15. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [A >= 3 + B && B >= A] (?,2)
16. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [1 + B >= 3 + A && A >= 2 + B] (?,3)
17. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [1 + B >= 3 + A && 1 + B >= A] (?,3)
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
19. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [A >= 4 + B && 1 + B >= A] (?,3)
20. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [B >= 4 + A && 1 + A >= 1 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
22. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [1 + A >= 3 + B && 1 + A >= 1 + B] (?,3)
23. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [1 + A >= 3 + B && B >= 1 + A] (?,3)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[11->{12,13,14,15},12->{16,17,18,19},13->{20,21,22,23},14->{16,17,18,19},15->{20,21,22,23},16->{16,17,18
,19},17->{20,21,22,23},18->{16,17,18,19},19->{20,21,22,23},20->{16,17,18,19},21->{20,21,22,23},22->{16,17,18
,19},23->{20,21,22,23}]
Sizebounds:
(<11,0,A>, B) (<11,0,B>, A)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
+ Applied Processor:
ChainProcessor False [11,12,13,14,15,16,17,18,19,20,21,22,23]
+ Details:
We chained rule 11 to obtain the rules [24,25,26,27] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [B >= 3 + A && A >= 1 + B] (?,2)
13. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [B >= 3 + A && B >= A] (?,2)
14. evalwisebb6in(A,B) -> evalwisebb4in(A,B) [A >= 3 + B && A >= 1 + B] (?,2)
15. evalwisebb6in(A,B) -> evalwisebb5in(A,B) [A >= 3 + B && B >= A] (?,2)
16. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [1 + B >= 3 + A && A >= 2 + B] (?,3)
17. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [1 + B >= 3 + A && 1 + B >= A] (?,3)
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
19. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [A >= 4 + B && 1 + B >= A] (?,3)
20. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [B >= 4 + A && 1 + A >= 1 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
22. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [1 + A >= 3 + B && 1 + A >= 1 + B] (?,3)
23. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [1 + A >= 3 + B && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[12->{16,17,18,19},13->{20,21,22,23},14->{16,17,18,19},15->{20,21,22,23},16->{16,17,18,19},17->{20,21,22
,23},18->{16,17,18,19},19->{20,21,22,23},20->{16,17,18,19},21->{20,21,22,23},22->{16,17,18,19},23->{20,21,22
,23},24->{16,17,18,19},25->{20,21,22,23},26->{16,17,18,19},27->{20,21,22,23}]
Sizebounds:
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<25,0,A>, ?) (<25,0,B>, ?)
(<26,0,A>, ?) (<26,0,B>, ?)
(<27,0,A>, ?) (<27,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [12,13,14,15]
* Step 15: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [1 + B >= 3 + A && A >= 2 + B] (?,3)
17. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [1 + B >= 3 + A && 1 + B >= A] (?,3)
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
19. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [A >= 4 + B && 1 + B >= A] (?,3)
20. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [B >= 4 + A && 1 + A >= 1 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
22. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [1 + A >= 3 + B && 1 + A >= 1 + B] (?,3)
23. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [1 + A >= 3 + B && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[16->{16,17,18,19},17->{20,21,22,23},18->{16,17,18,19},19->{20,21,22,23},20->{16,17,18,19},21->{20,21,22
,23},22->{16,17,18,19},23->{20,21,22,23},24->{16,17,18,19},25->{20,21,22,23},26->{16,17,18,19},27->{20,21,22
,23}]
Sizebounds:
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<25,0,A>, ?) (<25,0,B>, ?)
(<26,0,A>, ?) (<26,0,B>, ?)
(<27,0,A>, ?) (<27,0,B>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(16,16)
,(16,17)
,(16,18)
,(16,19)
,(17,20)
,(17,22)
,(17,23)
,(18,16)
,(18,17)
,(18,19)
,(19,20)
,(19,21)
,(19,22)
,(19,23)
,(20,16)
,(20,17)
,(20,18)
,(20,19)
,(21,20)
,(21,22)
,(21,23)
,(22,16)
,(22,17)
,(22,19)
,(23,20)
,(23,21)
,(23,22)
,(23,23)
,(24,16)
,(24,17)
,(24,18)
,(24,19)
,(25,20)
,(25,22)
,(25,23)
,(26,16)
,(26,17)
,(26,19)
,(27,20)
,(27,21)
,(27,22)
,(27,23)]
* Step 16: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [1 + B >= 3 + A && A >= 2 + B] (?,3)
17. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [1 + B >= 3 + A && 1 + B >= A] (?,3)
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
19. evalwisebb4in(A,B) -> evalwisebb5in(A,1 + B) [A >= 4 + B && 1 + B >= A] (?,3)
20. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [B >= 4 + A && 1 + A >= 1 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
22. evalwisebb5in(A,B) -> evalwisebb4in(1 + A,B) [1 + A >= 3 + B && 1 + A >= 1 + B] (?,3)
23. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [1 + A >= 3 + B && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[16->{},17->{21},18->{18},19->{},20->{},21->{21},22->{18},23->{},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<25,0,A>, ?) (<25,0,B>, ?)
(<26,0,A>, ?) (<26,0,B>, ?)
(<27,0,A>, ?) (<27,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [16,17,19,20,22,23]
* Step 17: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, ?) (<18,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<25,0,A>, ?) (<25,0,B>, ?)
(<26,0,A>, ?) (<26,0,B>, ?)
(<27,0,A>, ?) (<27,0,B>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<18,0,A>, A, .= 0) (<18,0,B>, 1 + B, .+ 1)
(<21,0,A>, 1 + A, .+ 1) (<21,0,B>, B, .= 0)
(<24,0,A>, B, .= 0) (<24,0,B>, A, .= 0)
(<25,0,A>, B, .= 0) (<25,0,B>, A, .= 0)
(<26,0,A>, B, .= 0) (<26,0,B>, A, .= 0)
(<27,0,A>, B, .= 0) (<27,0,B>, A, .= 0)
* Step 18: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, ?) (<18,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<25,0,A>, ?) (<25,0,B>, ?)
(<26,0,A>, ?) (<26,0,B>, ?)
(<27,0,A>, ?) (<27,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
* Step 19: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 18 : [A >= B && False] 21 : [B >= 3 + A
&& False] 24 : True 25 : True 26 : True 27 : True .
* Step 20: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (?,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwisebb4in) = 0
p(evalwisebb5in) = -1*x1 + x2
p(evalwisestart) = x1
The following rules are strictly oriented:
[B >= 4 + A && B >= 1 + A] ==>
evalwisebb5in(A,B) = -1*A + B
> -1 + -1*A + B
= evalwisebb5in(1 + A,B)
The following rules are weakly oriented:
[A >= 4 + B && A >= 2 + B] ==>
evalwisebb4in(A,B) = 0
>= 0
= evalwisebb4in(A,1 + B)
[A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] ==>
evalwisestart(A,B) = A
>= 0
= evalwisebb4in(B,A)
[A >= 0 && B >= 0 && A >= 3 + B && A >= B] ==>
evalwisestart(A,B) = A
>= A + -1*B
= evalwisebb5in(B,A)
[A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] ==>
evalwisestart(A,B) = A
>= 0
= evalwisebb4in(B,A)
[A >= 0 && B >= 0 && B >= 3 + A && A >= B] ==>
evalwisestart(A,B) = A
>= A + -1*B
= evalwisebb5in(B,A)
* Step 21: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (?,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (A,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwisebb4in) = x1 + -1*x2
p(evalwisebb5in) = 0
p(evalwisestart) = 1 + x2
The following rules are strictly oriented:
[A >= 4 + B && A >= 2 + B] ==>
evalwisebb4in(A,B) = A + -1*B
> -1 + A + -1*B
= evalwisebb4in(A,1 + B)
[A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] ==>
evalwisestart(A,B) = 1 + B
> -1*A + B
= evalwisebb4in(B,A)
[A >= 0 && B >= 0 && A >= 3 + B && A >= B] ==>
evalwisestart(A,B) = 1 + B
> 0
= evalwisebb5in(B,A)
[A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] ==>
evalwisestart(A,B) = 1 + B
> -1*A + B
= evalwisebb4in(B,A)
[A >= 0 && B >= 0 && B >= 3 + A && A >= B] ==>
evalwisestart(A,B) = 1 + B
> 0
= evalwisebb5in(B,A)
The following rules are weakly oriented:
[B >= 4 + A && B >= 1 + A] ==>
evalwisebb5in(A,B) = 0
>= 0
= evalwisebb5in(1 + A,B)
* Step 22: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (1 + B,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (A,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
+ Applied Processor:
LoopRecurrenceProcessor [21]
+ Details:
Applying the recurrence pattern linear * f to the expression B-A yields the solution -1*A + B .
* Step 23: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (1 + B,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (A,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
+ Applied Processor:
LoopRecurrenceProcessor [18]
+ Details:
Applying the recurrence pattern linear * f to the expression A-B yields the solution A + -1*B .
* Step 24: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. evalwisebb4in(A,B) -> evalwisebb4in(A,1 + B) [A >= 4 + B && A >= 2 + B] (1 + B,3)
21. evalwisebb5in(A,B) -> evalwisebb5in(1 + A,B) [B >= 4 + A && B >= 1 + A] (A,3)
24. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && B >= 1 + A] (1,4)
25. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && A >= 3 + B && A >= B] (1,4)
26. evalwisestart(A,B) -> evalwisebb4in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && B >= 1 + A] (1,4)
27. evalwisestart(A,B) -> evalwisebb5in(B,A) [A >= 0 && B >= 0 && B >= 3 + A && A >= B] (1,4)
Signature:
{(evalwisebb3in,2)
;(evalwisebb4in,2)
;(evalwisebb5in,2)
;(evalwisebb6in,2)
;(evalwiseentryin,2)
;(evalwisereturnin,2)
;(evalwisestart,2)
;(evalwisestop,2)}
Flow Graph:
[18->{18},21->{21},24->{},25->{21},26->{18},27->{}]
Sizebounds:
(<18,0,A>, B) (<18,0,B>, B)
(<21,0,A>, A) (<21,0,B>, A)
(<24,0,A>, B) (<24,0,B>, A)
(<25,0,A>, B) (<25,0,B>, A)
(<26,0,A>, B) (<26,0,B>, A)
(<27,0,A>, B) (<27,0,B>, A)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))