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