WORST_CASE(?,O(n^2))
* Step 1: UnsatRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1)
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1)
&& E >= 1
&& C >= 1 + J
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
13. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1 + H,I,J,K,L) [A >= 1 + F (?,1)
&& E >= 1 + H
&& A + C >= 1 + F
&& A >= 0
&& E >= H
&& F >= A
&& H >= 1
&& J = F
&& L = A
&& D = E
&& B = C]
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[0->{},1->{},2->{},3->{},4->{7,8,9,10},5->{11,12,13},6->{14,15},7->{},8->{7,8,9,10},9->{11,12,13},10->{14
,15},11->{7,8,9,10},12->{11,12,13},13->{14,15},14->{11,12,13},15->{14,15},16->{0,1,2,3,4,5,6}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [13]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1)
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1)
&& E >= 1
&& C >= 1 + J
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[0->{},1->{},2->{},3->{},4->{7,8,9,10},5->{11,12},6->{14,15},7->{},8->{7,8,9,10},9->{11,12},10->{14,15}
,11->{7,8,9,10},12->{11,12},14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}]
+ 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) (< 0,0,G>, G, .= 0) (< 0,0,H>, H, .= 0) (< 0,0,I>, I, .= 0) (< 0,0,J>, J, .= 0) (< 0,0,K>, K, .= 0) (< 0,0,L>, L, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, D, .= 0) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) (< 1,0,G>, G, .= 0) (< 1,0,H>, H, .= 0) (< 1,0,I>, I, .= 0) (< 1,0,J>, J, .= 0) (< 1,0,K>, K, .= 0) (< 1,0,L>, L, .= 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) (< 2,0,G>, G, .= 0) (< 2,0,H>, H, .= 0) (< 2,0,I>, I, .= 0) (< 2,0,J>, J, .= 0) (< 2,0,K>, K, .= 0) (< 2,0,L>, L, .= 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) (< 3,0,G>, G, .= 0) (< 3,0,H>, H, .= 0) (< 3,0,I>, I, .= 0) (< 3,0,J>, 0, .= 0) (< 3,0,K>, K, .= 0) (< 3,0,L>, L, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) (< 4,0,G>, G, .= 0) (< 4,0,H>, 0, .= 0) (< 4,0,I>, I, .= 0) (< 4,0,J>, 1, .= 1) (< 4,0,K>, K, .= 0) (< 4,0,L>, L, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, 0, .= 0) (< 5,0,G>, G, .= 0) (< 5,0,H>, 1, .= 1) (< 5,0,I>, I, .= 0) (< 5,0,J>, 0, .= 0) (< 5,0,K>, K, .= 0) (< 5,0,L>, L, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 6,0,F>, 1, .= 1) (< 6,0,G>, G, .= 0) (< 6,0,H>, 1, .= 1) (< 6,0,I>, I, .= 0) (< 6,0,J>, 0, .= 0) (< 6,0,K>, K, .= 0) (< 6,0,L>, L, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0) (< 7,0,H>, H, .= 0) (< 7,0,I>, I, .= 0) (< 7,0,J>, J, .= 0) (< 7,0,K>, K, .= 0) (< 7,0,L>, L, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0) (< 8,0,H>, 0, .= 0) (< 8,0,I>, I, .= 0) (< 8,0,J>, 1 + J, .+ 1) (< 8,0,K>, K, .= 0) (< 8,0,L>, L, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, J, .= 0) (< 9,0,G>, G, .= 0) (< 9,0,H>, 1, .= 1) (< 9,0,I>, I, .= 0) (< 9,0,J>, J, .= 0) (< 9,0,K>, K, .= 0) (< 9,0,L>, L, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, 1 + J, .+ 1) (<10,0,G>, G, .= 0) (<10,0,H>, 1, .= 1) (<10,0,I>, I, .= 0) (<10,0,J>, J, .= 0) (<10,0,K>, K, .= 0) (<10,0,L>, L, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0) (<11,0,I>, I, .= 0) (<11,0,J>, 1 + J, .+ 1) (<11,0,K>, K, .= 0) (<11,0,L>, L, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, J, .= 0) (<12,0,G>, G, .= 0) (<12,0,H>, 2 + H, .+ 2) (<12,0,I>, I, .= 0) (<12,0,J>, J, .= 0) (<12,0,K>, K, .= 0) (<12,0,L>, L, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0) (<14,0,E>, E, .= 0) (<14,0,F>, F, .= 0) (<14,0,G>, G, .= 0) (<14,0,H>, H, .= 0) (<14,0,I>, I, .= 0) (<14,0,J>, F, .= 0) (<14,0,K>, K, .= 0) (<14,0,L>, L, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0) (<15,0,E>, E, .= 0) (<15,0,F>, 1 + F, .+ 1) (<15,0,G>, G, .= 0) (<15,0,H>, H, .= 0) (<15,0,I>, I, .= 0) (<15,0,J>, J, .= 0) (<15,0,K>, K, .= 0) (<15,0,L>, L, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, C, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, E, .= 0) (<16,0,E>, E, .= 0) (<16,0,F>, G, .= 0) (<16,0,G>, G, .= 0) (<16,0,H>, I, .= 0) (<16,0,I>, I, .= 0) (<16,0,J>, K, .= 0) (<16,0,K>, K, .= 0) (<16,0,L>, A, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1)
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1)
&& E >= 1
&& C >= 1 + J
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[0->{},1->{},2->{},3->{},4->{7,8,9,10},5->{11,12},6->{14,15},7->{},8->{7,8,9,10},9->{11,12},10->{14,15}
,11->{7,8,9,10},12->{11,12},14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 0,0,G>, ?) (< 0,0,H>, ?) (< 0,0,I>, ?) (< 0,0,J>, ?) (< 0,0,K>, ?) (< 0,0,L>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 1,0,G>, ?) (< 1,0,H>, ?) (< 1,0,I>, ?) (< 1,0,J>, ?) (< 1,0,K>, ?) (< 1,0,L>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 2,0,G>, ?) (< 2,0,H>, ?) (< 2,0,I>, ?) (< 2,0,J>, ?) (< 2,0,K>, ?) (< 2,0,L>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 3,0,G>, ?) (< 3,0,H>, ?) (< 3,0,I>, ?) (< 3,0,J>, ?) (< 3,0,K>, ?) (< 3,0,L>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 4,0,G>, ?) (< 4,0,H>, ?) (< 4,0,I>, ?) (< 4,0,J>, ?) (< 4,0,K>, ?) (< 4,0,L>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?) (< 5,0,I>, ?) (< 5,0,J>, ?) (< 5,0,K>, ?) (< 5,0,L>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 6,0,H>, ?) (< 6,0,I>, ?) (< 6,0,J>, ?) (< 6,0,K>, ?) (< 6,0,L>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?) (< 7,0,I>, ?) (< 7,0,J>, ?) (< 7,0,K>, ?) (< 7,0,L>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?) (< 8,0,I>, ?) (< 8,0,J>, ?) (< 8,0,K>, ?) (< 8,0,L>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?) (< 9,0,G>, ?) (< 9,0,H>, ?) (< 9,0,I>, ?) (< 9,0,J>, ?) (< 9,0,K>, ?) (< 9,0,L>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, ?) (<10,0,I>, ?) (<10,0,J>, ?) (<10,0,K>, ?) (<10,0,L>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?) (<11,0,I>, ?) (<11,0,J>, ?) (<11,0,K>, ?) (<11,0,L>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, ?) (<12,0,I>, ?) (<12,0,J>, ?) (<12,0,K>, ?) (<12,0,L>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?) (<14,0,I>, ?) (<14,0,J>, ?) (<14,0,K>, ?) (<14,0,L>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<15,0,F>, ?) (<15,0,G>, ?) (<15,0,H>, ?) (<15,0,I>, ?) (<15,0,J>, ?) (<15,0,K>, ?) (<15,0,L>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, ?) (<16,0,F>, ?) (<16,0,G>, ?) (<16,0,H>, ?) (<16,0,I>, ?) (<16,0,J>, ?) (<16,0,K>, ?) (<16,0,L>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, I) (< 0,0,I>, I) (< 0,0,J>, K) (< 0,0,K>, K) (< 0,0,L>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, E) (< 1,0,E>, E) (< 1,0,F>, G) (< 1,0,G>, G) (< 1,0,H>, I) (< 1,0,I>, I) (< 1,0,J>, K) (< 1,0,K>, K) (< 1,0,L>, A)
(< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, E) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, I) (< 2,0,I>, I) (< 2,0,J>, K) (< 2,0,K>, K) (< 2,0,L>, A)
(< 3,0,A>, A) (< 3,0,B>, C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, G) (< 3,0,G>, G) (< 3,0,H>, I) (< 3,0,I>, I) (< 3,0,J>, 0) (< 3,0,K>, K) (< 3,0,L>, A)
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 7,0,A>, A) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, 2 + A + C + G) (< 7,0,G>, G) (< 7,0,H>, 1 + E) (< 7,0,I>, I) (< 7,0,J>, 2 + C) (< 7,0,K>, K) (< 7,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, 2 + C) (<10,0,G>, G) (<10,0,H>, 1) (<10,0,I>, I) (<10,0,J>, 2 + C) (<10,0,K>, K) (<10,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
* Step 4: UnsatPaths WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1)
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1)
&& E >= 1
&& C >= 1 + J
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[0->{},1->{},2->{},3->{},4->{7,8,9,10},5->{11,12},6->{14,15},7->{},8->{7,8,9,10},9->{11,12},10->{14,15}
,11->{7,8,9,10},12->{11,12},14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, I) (< 0,0,I>, I) (< 0,0,J>, K) (< 0,0,K>, K) (< 0,0,L>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, E) (< 1,0,E>, E) (< 1,0,F>, G) (< 1,0,G>, G) (< 1,0,H>, I) (< 1,0,I>, I) (< 1,0,J>, K) (< 1,0,K>, K) (< 1,0,L>, A)
(< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, E) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, I) (< 2,0,I>, I) (< 2,0,J>, K) (< 2,0,K>, K) (< 2,0,L>, A)
(< 3,0,A>, A) (< 3,0,B>, C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, G) (< 3,0,G>, G) (< 3,0,H>, I) (< 3,0,I>, I) (< 3,0,J>, 0) (< 3,0,K>, K) (< 3,0,L>, A)
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 7,0,A>, A) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, 2 + A + C + G) (< 7,0,G>, G) (< 7,0,H>, 1 + E) (< 7,0,I>, I) (< 7,0,J>, 2 + C) (< 7,0,K>, K) (< 7,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, 2 + C) (<10,0,G>, G) (<10,0,H>, 1) (<10,0,I>, I) (<10,0,J>, 2 + C) (<10,0,K>, K) (<10,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(4,9),(4,10),(8,9),(8,10),(11,8),(11,10)]
* Step 5: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1)
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1)
&& E >= 1
&& C >= 1 + J
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[0->{},1->{},2->{},3->{},4->{7,8},5->{11,12},6->{14,15},7->{},8->{7,8},9->{11,12},10->{14,15},11->{7,9}
,12->{11,12},14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, I) (< 0,0,I>, I) (< 0,0,J>, K) (< 0,0,K>, K) (< 0,0,L>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, E) (< 1,0,E>, E) (< 1,0,F>, G) (< 1,0,G>, G) (< 1,0,H>, I) (< 1,0,I>, I) (< 1,0,J>, K) (< 1,0,K>, K) (< 1,0,L>, A)
(< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, E) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, I) (< 2,0,I>, I) (< 2,0,J>, K) (< 2,0,K>, K) (< 2,0,L>, A)
(< 3,0,A>, A) (< 3,0,B>, C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, G) (< 3,0,G>, G) (< 3,0,H>, I) (< 3,0,I>, I) (< 3,0,J>, 0) (< 3,0,K>, K) (< 3,0,L>, A)
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 7,0,A>, A) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, 2 + A + C + G) (< 7,0,G>, G) (< 7,0,H>, 1 + E) (< 7,0,I>, I) (< 7,0,J>, 2 + C) (< 7,0,K>, K) (< 7,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<10,0,A>, A) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, 2 + C) (<10,0,G>, G) (<10,0,H>, 1) (<10,0,I>, I) (<10,0,J>, 2 + C) (<10,0,K>, K) (<10,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [10]
* Step 6: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1)
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[0->{},1->{},2->{},3->{},4->{7,8},5->{11,12},6->{14,15},7->{},8->{7,8},9->{11,12},11->{7,9},12->{11,12}
,14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, I) (< 0,0,I>, I) (< 0,0,J>, K) (< 0,0,K>, K) (< 0,0,L>, A)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, E) (< 1,0,E>, E) (< 1,0,F>, G) (< 1,0,G>, G) (< 1,0,H>, I) (< 1,0,I>, I) (< 1,0,J>, K) (< 1,0,K>, K) (< 1,0,L>, A)
(< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, E) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, I) (< 2,0,I>, I) (< 2,0,J>, K) (< 2,0,K>, K) (< 2,0,L>, A)
(< 3,0,A>, A) (< 3,0,B>, C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, G) (< 3,0,G>, G) (< 3,0,H>, I) (< 3,0,I>, I) (< 3,0,J>, 0) (< 3,0,K>, K) (< 3,0,L>, A)
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 7,0,A>, A) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, 2 + A + C + G) (< 7,0,G>, G) (< 7,0,H>, 1 + E) (< 7,0,I>, I) (< 7,0,J>, 2 + C) (< 7,0,K>, K) (< 7,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [0,1,2,3,7]
* Step 7: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = x1 + -1*x6
p(lbl121) = 0
p(lbl131) = 0
p(start) = x1
p(start0) = x1
The following rules are strictly oriented:
[A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] ==>
lbl111(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*F
> -1 + A + -1*F
= lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L)
The following rules are weakly oriented:
[A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = A
>= 0
= lbl131(A,B,C,D,E,F,G,0,I,1,K,L)
[E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = A
>= 0
= lbl121(A,B,C,D,E,0,G,1,I,0,K,L)
[A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = A
>= -1 + A
= lbl111(A,B,C,D,E,1,G,1,I,0,K,L)
[C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] ==>
lbl131(A,B,C,D,E,F,G,H,I,J,K,L) = 0
>= 0
= lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L)
[E >= 1 ==>
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
lbl131(A,B,C,D,E,F,G,H,I,J,K,L) = 0
>= 0
= lbl121(A,B,C,D,E,J,G,1,I,J,K,L)
[A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = 0
>= 0
= lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L)
[E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = 0
>= 0
= lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L)
[A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] ==>
lbl111(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*F
>= 0
= lbl121(A,B,C,D,E,F,G,H,I,F,K,L)
True ==>
start0(A,B,C,D,E,F,G,H,I,J,K,L) = A
>= A
= start(A,C,C,E,E,G,G,I,I,K,K,A)
* Step 8: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (A,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (1,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (1,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (1,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (1 + A,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (A,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = x1 + x2 + -1*x10
p(lbl121) = x1 + x2 + -1*x6
p(lbl131) = x1 + x2 + -1*x10
p(start) = x1 + x3
p(start0) = x1 + x3
The following rules are strictly oriented:
[A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = A + C
> -1 + A + B
= lbl131(A,B,C,D,E,F,G,0,I,1,K,L)
[A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*F
> -1 + A + B + -1*J
= lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L)
[A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] ==>
lbl111(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
> A + B + -1*F
= lbl121(A,B,C,D,E,F,G,H,I,F,K,L)
The following rules are weakly oriented:
[E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = A + C
>= A + B
= lbl121(A,B,C,D,E,0,G,1,I,0,K,L)
[A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = A + C
>= A + B
= lbl111(A,B,C,D,E,1,G,1,I,0,K,L)
[C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] ==>
lbl131(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
>= -1 + A + B + -1*J
= lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L)
[E >= 1 ==>
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
lbl131(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
>= A + B + -1*J
= lbl121(A,B,C,D,E,J,G,1,I,J,K,L)
[E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*F
>= A + B + -1*J
= lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L)
[A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] ==>
lbl111(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
>= A + B + -1*J
= lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L)
True ==>
start0(A,B,C,D,E,F,G,H,I,J,K,L) = A + C
>= A + C
= start(A,C,C,E,E,G,G,I,I,K,K,A)
* Step 10: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (1,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (1,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (1,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (A + C,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (1 + A,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (A,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 11: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (1,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (1,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (1,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (A + C,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (A + C,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (1 + A,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (A,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = x1 + x3 + -1*x10
p(lbl121) = x1 + x2 + -1*x10
p(lbl131) = x1 + x2 + -1*x10
p(start) = -1 + x1 + 2*x3
p(start0) = -1 + x1 + 2*x3
The following rules are strictly oriented:
[A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + 2*C
> -1 + A + B
= lbl131(A,B,C,D,E,F,G,0,I,1,K,L)
[C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] ==>
lbl131(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
> -1 + A + B + -1*J
= lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L)
[A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
> -1 + A + B + -1*J
= lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L)
[A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] ==>
lbl111(A,B,C,D,E,F,G,H,I,J,K,L) = A + C + -1*J
> A + B + -1*F
= lbl121(A,B,C,D,E,F,G,H,I,F,K,L)
The following rules are weakly oriented:
[E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + 2*C
>= A + B
= lbl121(A,B,C,D,E,0,G,1,I,0,K,L)
[A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] ==>
start(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + 2*C
>= A + C
= lbl111(A,B,C,D,E,1,G,1,I,0,K,L)
[E >= 1 ==>
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
lbl131(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
>= A + B + -1*J
= lbl121(A,B,C,D,E,J,G,1,I,J,K,L)
[E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = A + B + -1*J
>= A + B + -1*J
= lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L)
[A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] ==>
lbl111(A,B,C,D,E,F,G,H,I,J,K,L) = A + C + -1*J
>= A + C + -1*J
= lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L)
True ==>
start0(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + 2*C
>= -1 + A + 2*C
= start(A,C,C,E,E,G,G,I,I,K,K,A)
* Step 12: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (1,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (1,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (1,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (1 + A + 2*C,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (A + C,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (A + C,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (1 + A,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (A,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [12], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl121) = 1 + x5 + -1*x8
The following rules are strictly oriented:
[E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] ==>
lbl121(A,B,C,D,E,F,G,H,I,J,K,L) = 1 + E + -1*H
> E + -1*H
= lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
* Step 13: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (1,1)
5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (1,1)
6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (1,1)
8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (1 + A + 2*C,1)
9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (A + C,1)
&& C >= 1 + J
&& J >= A
&& E >= 0
&& A >= 0
&& C >= 1
&& A + C >= J
&& J >= 1
&& H = E
&& L = A
&& D = E
&& B = C]
11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (A + C,1)
12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (4 + 4*A + 2*A*E + 2*C + C*E + 2*E,1)
14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (1 + A,1)
15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (A,1)
16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1)
Signature:
{(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)}
Flow Graph:
[4->{8},5->{11,12},6->{14,15},8->{8},9->{11,12},11->{9},12->{11,12},14->{11,12},15->{14,15},16->{4,5,6}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, E) (< 4,0,E>, E) (< 4,0,F>, G) (< 4,0,G>, G) (< 4,0,H>, 0) (< 4,0,I>, I) (< 4,0,J>, 1) (< 4,0,K>, K) (< 4,0,L>, A)
(< 5,0,A>, A) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, E) (< 5,0,E>, E) (< 5,0,F>, 0) (< 5,0,G>, G) (< 5,0,H>, 1) (< 5,0,I>, I) (< 5,0,J>, 0) (< 5,0,K>, K) (< 5,0,L>, A)
(< 6,0,A>, A) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, 1) (< 6,0,G>, G) (< 6,0,H>, 1) (< 6,0,I>, I) (< 6,0,J>, 0) (< 6,0,K>, K) (< 6,0,L>, A)
(< 8,0,A>, A) (< 8,0,B>, C) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, 2 + A + C + G) (< 8,0,G>, G) (< 8,0,H>, 0) (< 8,0,I>, I) (< 8,0,J>, C) (< 8,0,K>, K) (< 8,0,L>, A)
(< 9,0,A>, A) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, E) (< 9,0,E>, E) (< 9,0,F>, 2 + C) (< 9,0,G>, G) (< 9,0,H>, 1) (< 9,0,I>, I) (< 9,0,J>, C) (< 9,0,K>, K) (< 9,0,L>, A)
(<11,0,A>, A) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, 2 + A + C) (<11,0,G>, G) (<11,0,H>, 1 + E) (<11,0,I>, I) (<11,0,J>, 2 + C) (<11,0,K>, K) (<11,0,L>, A)
(<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, 1 + C) (<12,0,G>, G) (<12,0,H>, E) (<12,0,I>, I) (<12,0,J>, 1 + C) (<12,0,K>, K) (<12,0,L>, A)
(<14,0,A>, A) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, E) (<14,0,E>, E) (<14,0,F>, 2 + A + C) (<14,0,G>, G) (<14,0,H>, 1) (<14,0,I>, I) (<14,0,J>, 1) (<14,0,K>, K) (<14,0,L>, A)
(<15,0,A>, A) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, E) (<15,0,E>, E) (<15,0,F>, A) (<15,0,G>, G) (<15,0,H>, 1) (<15,0,I>, I) (<15,0,J>, A) (<15,0,K>, K) (<15,0,L>, A)
(<16,0,A>, A) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, E) (<16,0,E>, E) (<16,0,F>, G) (<16,0,G>, G) (<16,0,H>, I) (<16,0,I>, I) (<16,0,J>, K) (<16,0,K>, K) (<16,0,L>, A)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))