WORST_CASE(?,O(n^1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B,C) -> f2(-1 + A,B,C) [A >= 31] (?,1)
1. f2(A,B,C) -> f300(A,-1 + B,C) [30 >= A] (?,1)
2. f300(A,B,C) -> f2(A,B,C) [B >= 21] (?,1)
3. f300(A,B,C) -> f1(A,B,D) [20 >= B] (?,1)
4. f3(A,B,C) -> f300(A,B,C) True (1,1)
Signature:
{(f1,3);(f2,3);(f3,3);(f300,3)}
Flow Graph:
[0->{0,1},1->{2,3},2->{0,1},3->{},4->{2,3}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [C] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (?,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (?,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (?,1)
3. f300(A,B) -> f1(A,B) [20 >= B] (?,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2,3},2->{0,1},3->{},4->{2,3}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, 1 + A, .+ 1) (<0,0,B>, B, .= 0)
(<1,0,A>, A, .= 0) (<1,0,B>, 1 + B, .+ 1)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0)
(<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (?,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (?,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (?,1)
3. f300(A,B) -> f1(A,B) [20 >= B] (?,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2,3},2->{0,1},3->{},4->{2,3}]
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>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, 30) (<1,0,B>, ?)
(<2,0,A>, 30 + A) (<2,0,B>, ?)
(<3,0,A>, 30 + A) (<3,0,B>, ?)
(<4,0,A>, A) (<4,0,B>, B)
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (?,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (?,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (?,1)
3. f300(A,B) -> f1(A,B) [20 >= B] (?,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2,3},2->{0,1},3->{},4->{2,3}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, 30) (<1,0,B>, ?)
(<2,0,A>, 30 + A) (<2,0,B>, ?)
(<3,0,A>, 30 + A) (<3,0,B>, ?)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (?,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (?,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (?,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2},2->{0,1},4->{2}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, 30) (<1,0,B>, ?)
(<2,0,A>, 30 + A) (<2,0,B>, ?)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f2) = -21 + x2
p(f3) = -20 + x2
p(f300) = -20 + x2
The following rules are strictly oriented:
[B >= 21] ==>
f300(A,B) = -20 + B
> -21 + B
= f2(A,B)
The following rules are weakly oriented:
[A >= 31] ==>
f2(A,B) = -21 + B
>= -21 + B
= f2(-1 + A,B)
[30 >= A] ==>
f2(A,B) = -21 + B
>= -21 + B
= f300(A,-1 + B)
True ==>
f3(A,B) = -20 + B
>= -20 + B
= f300(A,B)
* Step 6: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (?,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (?,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (20 + B,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2},2->{0,1},4->{2}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, 30) (<1,0,B>, ?)
(<2,0,A>, 30 + A) (<2,0,B>, ?)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f2) = 1 + x1
p(f3) = 1 + x1
p(f300) = 1 + x1
The following rules are strictly oriented:
[A >= 31] ==>
f2(A,B) = 1 + A
> A
= f2(-1 + A,B)
The following rules are weakly oriented:
[30 >= A] ==>
f2(A,B) = 1 + A
>= 1 + A
= f300(A,-1 + B)
[B >= 21] ==>
f300(A,B) = 1 + A
>= 1 + A
= f2(A,B)
True ==>
f3(A,B) = 1 + A
>= 1 + A
= f300(A,B)
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (1 + A,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (?,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (20 + B,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2},2->{0,1},4->{2}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, 30) (<1,0,B>, ?)
(<2,0,A>, 30 + A) (<2,0,B>, ?)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 8: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f2(A,B) -> f2(-1 + A,B) [A >= 31] (1 + A,1)
1. f2(A,B) -> f300(A,-1 + B) [30 >= A] (21 + A + B,1)
2. f300(A,B) -> f2(A,B) [B >= 21] (20 + B,1)
4. f3(A,B) -> f300(A,B) True (1,1)
Signature:
{(f1,2);(f2,2);(f3,2);(f300,2)}
Flow Graph:
[0->{0,1},1->{2},2->{0,1},4->{2}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, 30) (<1,0,B>, ?)
(<2,0,A>, 30 + A) (<2,0,B>, ?)
(<4,0,A>, A) (<4,0,B>, B)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))