WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
1. a0(A,B) -> a(A,B) True (?,1)
2. a1(A,B) -> a(B,B) True (?,1)
3. a(A,B) -> c2(a0(C,D),a1(C,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,1)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{3},1->{3},2->{3},3->{1,2}]
+ 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>, B, .= 0) (<2,0,B>, B, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, A, .= 0)
(<3,1,A>, A, .= 0) (<3,1,B>, A, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
1. a0(A,B) -> a(A,B) True (?,1)
2. a1(A,B) -> a(B,B) True (?,1)
3. a(A,B) -> c2(a0(C,D),a1(C,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,1)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{3},1->{3},2->{3},3->{1,2}]
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>, ?)
(<3,1,A>, ?) (<3,1,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>, A) (<3,0,B>, A)
(<3,1,A>, A) (<3,1,B>, A)
* Step 3: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
1. a0(A,B) -> a(A,B) True (?,1)
2. a1(A,B) -> a(B,B) True (?,1)
3. a(A,B) -> c2(a0(C,D),a1(C,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,1)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{3},1->{3},2->{3},3->{1,2}]
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>, A) (<3,0,B>, A)
(<3,1,A>, A) (<3,1,B>, A)
+ Applied Processor:
ChainProcessor False [0,1,2,3]
+ Details:
We chained rule 3 to obtain the rules [4] .
* Step 4: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
1. a0(A,B) -> a(A,B) True (?,1)
2. a1(A,B) -> a(B,B) True (?,1)
4. a(A,B) -> c2(a(C,D),a1(C,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,2)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{4},1->{4},2->{4},4->{2,4}]
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)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
UnreachableRules
+ Details:
Following transitions are not reachable from the starting states and are removed: [1]
* Step 5: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
2. a1(A,B) -> a(B,B) True (?,1)
4. a(A,B) -> c2(a(C,D),a1(C,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,2)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{4},2->{4},4->{2,4}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<2,0,A>, A) (<2,0,B>, B)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
ChainProcessor False [0,2,4]
+ Details:
We chained rule 4 to obtain the rules [5] .
* Step 6: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
2. a1(A,B) -> a(B,B) True (?,1)
5. a(A,B) -> c2(a(C,D),a(D,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,3)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{5},2->{5},5->{5}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<2,0,A>, A) (<2,0,B>, B)
(<5,0,A>, A) (<5,0,B>, B)
+ Applied Processor:
UnreachableRules
+ Details:
Following transitions are not reachable from the starting states and are removed: [2]
* Step 7: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
5. a(A,B) -> c2(a(C,D),a(D,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,3)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{5},5->{5}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<5,0,A>, A) (<5,0,B>, B)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, A, .= 0) (<0,0,B>, B, .= 0)
(<5,0,A>, A, .= 0) (<5,0,B>, A, .= 0)
(<5,1,A>, A, .= 0) (<5,1,B>, A, .= 0)
* Step 8: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
5. a(A,B) -> c2(a(C,D),a(D,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,3)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{5},5->{5}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<5,0,A>, ?) (<5,0,B>, ?)
(<5,1,A>, ?) (<5,1,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, B)
(<5,0,A>, A) (<5,0,B>, A)
(<5,1,A>, A) (<5,1,B>, A)
* Step 9: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
5. a(A,B) -> c2(a(C,D),a(D,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (?,3)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{5},5->{5}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<5,0,A>, A) (<5,0,B>, A)
(<5,1,A>, A) (<5,1,B>, A)
+ Applied Processor:
LoopRecurrenceProcessor [5]
+ Details:
Solving the recurrence Master Theorem (A) for the expression A yields the solution A .
* Step 10: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B) -> a(A,B) [A >= 0] (1,1)
5. a(A,B) -> c2(a(C,D),a(D,D)) [A >= 1 && A >= 2*C && A >= 2*D && C >= 0 && D >= 0] (A,3)
Signature:
{(a,2);(a0,2);(a1,2);(start,2)}
Flow Graph:
[0->{5},5->{5}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<5,0,A>, A) (<5,0,B>, A)
(<5,1,A>, A) (<5,1,B>, A)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))