WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. power(A) -> m0(A) True (?,1)
1. m0(A) -> m2(A) True (?,1)
2. m3(A) -> m1(A) [A = 0] (?,1)
3. m4(A) -> c2(m1(B),power(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
6. m5(A) -> m3(A) True (?,1)
7. start(A) -> power(A) True (1,1)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[0->{1},1->{4},2->{},3->{0},4->{5,6},5->{3},6->{2},7->{0}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, A, .= 0)
(<1,0,A>, A, .= 0)
(<2,0,A>, A, .= 0)
(<3,0,A>, 1 + A, .+ 1)
(<3,1,A>, 1 + A, .+ 1)
(<4,0,A>, A, .= 0)
(<5,0,A>, A, .= 0)
(<6,0,A>, A, .= 0)
(<7,0,A>, A, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. power(A) -> m0(A) True (?,1)
1. m0(A) -> m2(A) True (?,1)
2. m3(A) -> m1(A) [A = 0] (?,1)
3. m4(A) -> c2(m1(B),power(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
6. m5(A) -> m3(A) True (?,1)
7. start(A) -> power(A) True (1,1)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[0->{1},1->{4},2->{},3->{0},4->{5,6},5->{3},6->{2},7->{0}]
Sizebounds:
(<0,0,A>, ?)
(<1,0,A>, ?)
(<2,0,A>, ?)
(<3,0,A>, ?)
(<3,1,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<6,0,A>, ?)
(<7,0,A>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, ?)
(<1,0,A>, ?)
(<2,0,A>, ?)
(<3,0,A>, ?)
(<3,1,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<6,0,A>, ?)
(<7,0,A>, A)
* Step 3: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. power(A) -> m0(A) True (?,1)
1. m0(A) -> m2(A) True (?,1)
2. m3(A) -> m1(A) [A = 0] (?,1)
3. m4(A) -> c2(m1(B),power(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
6. m5(A) -> m3(A) True (?,1)
7. start(A) -> power(A) True (1,1)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[0->{1},1->{4},2->{},3->{0},4->{5,6},5->{3},6->{2},7->{0}]
Sizebounds:
(<0,0,A>, ?)
(<1,0,A>, ?)
(<2,0,A>, ?)
(<3,0,A>, ?)
(<3,1,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<6,0,A>, ?)
(<7,0,A>, A)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [6,2]
* Step 4: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. power(A) -> m0(A) True (?,1)
1. m0(A) -> m2(A) True (?,1)
3. m4(A) -> c2(m1(B),power(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
7. start(A) -> power(A) True (1,1)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[0->{1},1->{4},3->{0},4->{5},5->{3},7->{0}]
Sizebounds:
(<0,0,A>, ?)
(<1,0,A>, ?)
(<3,0,A>, ?)
(<3,1,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<7,0,A>, A)
+ Applied Processor:
ChainProcessor False [0,1,3,4,5,7]
+ Details:
We chained rule 0 to obtain the rules [8] .
* Step 5: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. m0(A) -> m2(A) True (?,1)
3. m4(A) -> c2(m1(B),power(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
7. start(A) -> power(A) True (1,1)
8. power(A) -> m2(A) True (?,2)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[1->{4},3->{8},4->{5},5->{3},7->{8},8->{4}]
Sizebounds:
(<1,0,A>, ?)
(<3,0,A>, ?)
(<3,1,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<7,0,A>, A)
(<8,0,A>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [1]
* Step 6: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. m4(A) -> c2(m1(B),power(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
7. start(A) -> power(A) True (1,1)
8. power(A) -> m2(A) True (?,2)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[3->{8},4->{5},5->{3},7->{8},8->{4}]
Sizebounds:
(<3,0,A>, ?)
(<3,1,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<7,0,A>, A)
(<8,0,A>, ?)
+ Applied Processor:
ChainProcessor False [3,4,5,7,8]
+ Details:
We chained rule 3 to obtain the rules [9] .
* Step 7: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. m2(A) -> m5(A) True (?,1)
5. m5(A) -> m4(A) True (?,1)
7. start(A) -> power(A) True (1,1)
8. power(A) -> m2(A) True (?,2)
9. m4(A) -> c2(m1(B),m2(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,3)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[4->{5},5->{9},7->{8},8->{4},9->{4}]
Sizebounds:
(<4,0,A>, ?)
(<5,0,A>, ?)
(<7,0,A>, A)
(<8,0,A>, ?)
(<9,0,A>, ?)
+ Applied Processor:
ChainProcessor False [4,5,7,8,9]
+ Details:
We chained rule 4 to obtain the rules [10] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
5. m5(A) -> m4(A) True (?,1)
7. start(A) -> power(A) True (1,1)
8. power(A) -> m2(A) True (?,2)
9. m4(A) -> c2(m1(B),m2(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,3)
10. m2(A) -> m4(A) True (?,2)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[5->{9},7->{8},8->{10},9->{10},10->{9}]
Sizebounds:
(< 5,0,A>, ?)
(< 7,0,A>, A)
(< 8,0,A>, ?)
(< 9,0,A>, ?)
(<10,0,A>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [5]
* Step 9: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
7. start(A) -> power(A) True (1,1)
8. power(A) -> m2(A) True (?,2)
9. m4(A) -> c2(m1(B),m2(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,3)
10. m2(A) -> m4(A) True (?,2)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[7->{8},8->{10},9->{10},10->{9}]
Sizebounds:
(< 7,0,A>, A)
(< 8,0,A>, ?)
(< 9,0,A>, ?)
(<10,0,A>, ?)
+ Applied Processor:
ChainProcessor False [7,8,9,10]
+ Details:
We chained rule 7 to obtain the rules [11] .
* Step 10: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
8. power(A) -> m2(A) True (?,2)
9. m4(A) -> c2(m1(B),m2(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,3)
10. m2(A) -> m4(A) True (?,2)
11. start(A) -> m2(A) True (1,3)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[8->{10},9->{10},10->{9},11->{10}]
Sizebounds:
(< 8,0,A>, ?)
(< 9,0,A>, ?)
(<10,0,A>, ?)
(<11,0,A>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [8]
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
9. m4(A) -> c2(m1(B),m2(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,3)
10. m2(A) -> m4(A) True (?,2)
11. start(A) -> m2(A) True (1,3)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[9->{10},10->{9},11->{10}]
Sizebounds:
(< 9,0,A>, ?)
(<10,0,A>, ?)
(<11,0,A>, ?)
+ Applied Processor:
ChainProcessor False [9,10,11]
+ Details:
We chained rule 9 to obtain the rules [12] .
* Step 12: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
10. m2(A) -> m4(A) True (?,2)
11. start(A) -> m2(A) True (1,3)
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[10->{12},11->{10},12->{12}]
Sizebounds:
(<10,0,A>, ?)
(<11,0,A>, ?)
(<12,0,A>, ?)
+ Applied Processor:
ChainProcessor False [10,11,12]
+ Details:
We chained rule 11 to obtain the rules [13] .
* Step 13: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
10. m2(A) -> m4(A) True (?,2)
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,5)
13. start(A) -> m4(A) True (1,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[10->{12},12->{12},13->{12}]
Sizebounds:
(<10,0,A>, ?)
(<12,0,A>, ?)
(<13,0,A>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [10]
* Step 14: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,5)
13. start(A) -> m4(A) True (1,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[12->{12},13->{12}]
Sizebounds:
(<12,0,A>, ?)
(<13,0,A>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<12,0,A>, 1 + A, .+ 1)
(<12,1,A>, 1 + A, .+ 1)
(<13,0,A>, A, .= 0)
* Step 15: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,5)
13. start(A) -> m4(A) True (1,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[12->{12},13->{12}]
Sizebounds:
(<12,0,A>, ?)
(<12,1,A>, ?)
(<13,0,A>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<12,0,A>, ?)
(<12,1,A>, ?)
(<13,0,A>, A)
* Step 16: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,5)
13. start(A) -> m4(A) True (1,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[12->{12},13->{12}]
Sizebounds:
(<12,0,A>, ?)
(<12,1,A>, ?)
(<13,0,A>, A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 12 : True 13 : True .
* Step 17: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,5)
13. start(A) -> m4(A) True (1,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[12->{12},13->{12}]
Sizebounds:
(<12,0,A>, ?)
(<12,1,A>, ?)
(<13,0,A>, A)
+ Applied Processor:
LoopRecurrenceProcessor [12]
+ Details:
Applying the recurrence pattern linear * f to the expression A yields the solution A .
* Step 18: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. m4(A) -> c2(m1(B),m4(B)) [B >= 0 && A >= 1 + B && 1 + B >= A] (A,5)
13. start(A) -> m4(A) True (1,5)
Signature:
{(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(power,1);(start,1)}
Flow Graph:
[12->{12},13->{12}]
Sizebounds:
(<12,0,A>, ?)
(<12,1,A>, ?)
(<13,0,A>, A)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))