WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= A && B = A && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A >= 1 && B = A && C = D && E = F] (?,1)
2. lbl71(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= 1 + C && B = 0 && C + E = D + F && A + C = D] (?,1)
3. lbl71(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] (?,1)
4. start0(A,B,C,D,E,F) -> start(A,A,D,D,F,F) True (1,1)
Signature:
{(lbl71,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{},1->{2,3},2->{},3->{2,3},4->{0,1}]
+ 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) (<0,0,E>, E, .= 0) (<0,0,F>, F, .= 0)
(<1,0,A>, A, .= 0) (<1,0,B>, 1 + B, .+ 1) (<1,0,C>, 1 + C, .+ 1) (<1,0,D>, D, .= 0) (<1,0,E>, 1 + E, .+ 1) (<1,0,F>, F, .= 0)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0) (<2,0,E>, E, .= 0) (<2,0,F>, F, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, 1 + B, .+ 1) (<3,0,C>, 1 + C, .+ 1) (<3,0,D>, D, .= 0) (<3,0,E>, 1 + E, .+ 1) (<3,0,F>, F, .= 0)
(<4,0,A>, A, .= 0) (<4,0,B>, A, .= 0) (<4,0,C>, D, .= 0) (<4,0,D>, D, .= 0) (<4,0,E>, F, .= 0) (<4,0,F>, F, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= A && B = A && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A >= 1 && B = A && C = D && E = F] (?,1)
2. lbl71(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= 1 + C && B = 0 && C + E = D + F && A + C = D] (?,1)
3. lbl71(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] (?,1)
4. start0(A,B,C,D,E,F) -> start(A,A,D,D,F,F) True (1,1)
Signature:
{(lbl71,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{},1->{2,3},2->{},3->{2,3},4->{0,1}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) (<0,0,E>, ?) (<0,0,F>, ?)
(<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<1,0,E>, ?) (<1,0,F>, ?)
(<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) (<2,0,E>, ?) (<2,0,F>, ?)
(<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?) (<3,0,E>, ?) (<3,0,F>, ?)
(<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) (<4,0,E>, ?) (<4,0,F>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, A) (<0,0,C>, D) (<0,0,D>, D) (<0,0,E>, F) (<0,0,F>, F)
(<1,0,A>, A) (<1,0,B>, 1 + A) (<1,0,C>, 1 + D) (<1,0,D>, D) (<1,0,E>, 1 + F) (<1,0,F>, F)
(<2,0,A>, A) (<2,0,B>, 1 + A + D) (<2,0,C>, 1 + D) (<2,0,D>, D) (<2,0,E>, 1 + D + F) (<2,0,F>, F)
(<3,0,A>, A) (<3,0,B>, 1 + A + D) (<3,0,C>, D) (<3,0,D>, D) (<3,0,E>, 1 + D + F) (<3,0,F>, F)
(<4,0,A>, A) (<4,0,B>, A) (<4,0,C>, D) (<4,0,D>, D) (<4,0,E>, F) (<4,0,F>, F)
* Step 3: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= A && B = A && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A >= 1 && B = A && C = D && E = F] (?,1)
2. lbl71(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= 1 + C && B = 0 && C + E = D + F && A + C = D] (?,1)
3. lbl71(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] (?,1)
4. start0(A,B,C,D,E,F) -> start(A,A,D,D,F,F) True (1,1)
Signature:
{(lbl71,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{},1->{2,3},2->{},3->{2,3},4->{0,1}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, A) (<0,0,C>, D) (<0,0,D>, D) (<0,0,E>, F) (<0,0,F>, F)
(<1,0,A>, A) (<1,0,B>, 1 + A) (<1,0,C>, 1 + D) (<1,0,D>, D) (<1,0,E>, 1 + F) (<1,0,F>, F)
(<2,0,A>, A) (<2,0,B>, 1 + A + D) (<2,0,C>, 1 + D) (<2,0,D>, D) (<2,0,E>, 1 + D + F) (<2,0,F>, F)
(<3,0,A>, A) (<3,0,B>, 1 + A + D) (<3,0,C>, D) (<3,0,D>, D) (<3,0,E>, 1 + D + F) (<3,0,F>, F)
(<4,0,A>, A) (<4,0,B>, A) (<4,0,C>, D) (<4,0,D>, D) (<4,0,E>, F) (<4,0,F>, F)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [0,2]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A >= 1 && B = A && C = D && E = F] (?,1)
3. lbl71(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] (?,1)
4. start0(A,B,C,D,E,F) -> start(A,A,D,D,F,F) True (1,1)
Signature:
{(lbl71,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[1->{3},3->{3},4->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, 1 + A) (<1,0,C>, 1 + D) (<1,0,D>, D) (<1,0,E>, 1 + F) (<1,0,F>, F)
(<3,0,A>, A) (<3,0,B>, 1 + A + D) (<3,0,C>, D) (<3,0,D>, D) (<3,0,E>, 1 + D + F) (<3,0,F>, F)
(<4,0,A>, A) (<4,0,B>, A) (<4,0,C>, D) (<4,0,D>, D) (<4,0,E>, F) (<4,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl71) = x1 + x3 + -1*x4
p(start) = -1 + x1 + x3 + -1*x4
p(start0) = -1 + x1
The following rules are strictly oriented:
[A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] ==>
lbl71(A,B,C,D,E,F) = A + C + -1*D
> -1 + A + C + -1*D
= lbl71(A,-1 + B,-1 + C,D,1 + E,F)
The following rules are weakly oriented:
[A >= 1 && B = A && C = D && E = F] ==>
start(A,B,C,D,E,F) = -1 + A + C + -1*D
>= -1 + A + C + -1*D
= lbl71(A,-1 + B,-1 + C,D,1 + E,F)
True ==>
start0(A,B,C,D,E,F) = -1 + A
>= -1 + A
= start(A,A,D,D,F,F)
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A >= 1 && B = A && C = D && E = F] (?,1)
3. lbl71(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] (1 + A,1)
4. start0(A,B,C,D,E,F) -> start(A,A,D,D,F,F) True (1,1)
Signature:
{(lbl71,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[1->{3},3->{3},4->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, 1 + A) (<1,0,C>, 1 + D) (<1,0,D>, D) (<1,0,E>, 1 + F) (<1,0,F>, F)
(<3,0,A>, A) (<3,0,B>, 1 + A + D) (<3,0,C>, D) (<3,0,D>, D) (<3,0,E>, 1 + D + F) (<3,0,F>, F)
(<4,0,A>, A) (<4,0,B>, A) (<4,0,C>, D) (<4,0,D>, D) (<4,0,E>, F) (<4,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. start(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A >= 1 && B = A && C = D && E = F] (1,1)
3. lbl71(A,B,C,D,E,F) -> lbl71(A,-1 + B,-1 + C,D,1 + E,F) [A + C >= 1 + D && D >= 1 + C && A + C >= D && C + E = D + F && B + D = A + C] (1 + A,1)
4. start0(A,B,C,D,E,F) -> start(A,A,D,D,F,F) True (1,1)
Signature:
{(lbl71,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[1->{3},3->{3},4->{1}]
Sizebounds:
(<1,0,A>, A) (<1,0,B>, 1 + A) (<1,0,C>, 1 + D) (<1,0,D>, D) (<1,0,E>, 1 + F) (<1,0,F>, F)
(<3,0,A>, A) (<3,0,B>, 1 + A + D) (<3,0,C>, D) (<3,0,D>, D) (<3,0,E>, 1 + D + F) (<3,0,F>, F)
(<4,0,A>, A) (<4,0,B>, A) (<4,0,C>, D) (<4,0,D>, D) (<4,0,E>, F) (<4,0,F>, F)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))