WORST_CASE(?,O(1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. selectOrd(A,B,C,D,E) -> m4(A,B,C,D,E) [A >= 0] (1,1)
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (?,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (?,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
12. m1(A,B,C,D,E) -> m9(A,D,B,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. m3(A,B,C,D,E) -> m8(C,B,B,D,E) True (?,1)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[0->{7},1->{11,12},2->{16,17},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},12->{}
,13->{2},14->{1},15->{13,14},16->{15},17->{}]
+ 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)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, 1 + A, .+ 1) (< 1,0,E>, E, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, 2 + A, .+ 2) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, E, .= 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)
(< 4,0,A>, A, .= 0) (< 4,0,B>, C, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, 1 + B, .+ 1) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, 0, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0)
(< 6,1,A>, A, .= 0) (< 6,1,B>, B, .= 0) (< 6,1,C>, 0, .= 0) (< 6,1,D>, D, .= 0) (< 6,1,E>, E, .= 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)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, ?, .?) (< 8,0,E>, ?, .?)
(< 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)
(<10,0,A>, A, .= 0) (<10,0,B>, D, .= 0) (<10,0,C>, B, .= 0) (<10,0,D>, E, .= 0) (<10,0,E>, E, .= 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)
(<12,0,A>, A, .= 0) (<12,0,B>, D, .= 0) (<12,0,C>, B, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0)
(<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0) (<13,0,D>, D, .= 0) (<13,0,E>, E, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, D, .= 0) (<14,0,C>, B, .= 0) (<14,0,D>, D, .= 0) (<14,0,E>, E, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, C, .= 0) (<15,0,C>, 2 + A + C, .* 2) (<15,0,D>, 2 + A + C, .* 2) (<15,0,E>, E, .= 0)
(<15,1,A>, A, .= 0) (<15,1,B>, C, .= 0) (<15,1,C>, 2 + A + C, .* 2) (<15,1,D>, 2 + A + C, .* 2) (<15,1,E>, E, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0) (<16,0,E>, E, .= 0)
(<17,0,A>, C, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, B, .= 0) (<17,0,D>, D, .= 0) (<17,0,E>, E, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. selectOrd(A,B,C,D,E) -> m4(A,B,C,D,E) [A >= 0] (1,1)
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (?,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (?,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
12. m1(A,B,C,D,E) -> m9(A,D,B,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. m3(A,B,C,D,E) -> m8(C,B,B,D,E) True (?,1)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[0->{7},1->{11,12},2->{16,17},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},12->{}
,13->{2},14->{1},15->{13,14},16->{15},17->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?)
(< 6,1,A>, ?) (< 6,1,B>, ?) (< 6,1,C>, ?) (< 6,1,D>, ?) (< 6,1,E>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, ?)
(<15,1,A>, ?) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,E>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, D) (< 7,0,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<12,0,A>, A) (<12,0,B>, 1 + A) (<12,0,C>, A) (<12,0,D>, 1 + A) (<12,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, ?) (<17,0,B>, 2 + A) (<17,0,C>, 2 + A) (<17,0,D>, ?) (<17,0,E>, E)
* Step 3: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. selectOrd(A,B,C,D,E) -> m4(A,B,C,D,E) [A >= 0] (1,1)
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (?,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (?,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
12. m1(A,B,C,D,E) -> m9(A,D,B,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. m3(A,B,C,D,E) -> m8(C,B,B,D,E) True (?,1)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[0->{7},1->{11,12},2->{16,17},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},12->{}
,13->{2},14->{1},15->{13,14},16->{15},17->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, D) (< 7,0,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<12,0,A>, A) (<12,0,B>, 1 + A) (<12,0,C>, A) (<12,0,D>, 1 + A) (<12,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, ?) (<17,0,B>, 2 + A) (<17,0,C>, 2 + A) (<17,0,D>, ?) (<17,0,E>, E)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [12,17]
* Step 4: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. selectOrd(A,B,C,D,E) -> m4(A,B,C,D,E) [A >= 0] (1,1)
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (?,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (?,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[0->{7},1->{11},2->{16},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},13->{2}
,14->{1},15->{13,14},16->{15}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, D) (< 7,0,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(m0) = 0
p(m1) = 0
p(m2) = 1
p(m3) = 1
p(m4) = 2
p(m5) = 0
p(m6) = 0
p(m7) = 0
p(n0) = 0
p(n1) = 1
p(n2) = 0
p(n3) = 0
p(n4) = 1
p(n40) = 1
p(n41) = 0
p(selectOrd) = 2
The following rules are strictly oriented:
[A >= 0] ==>
m4(A,B,C,D,E) = 2
> 1
= n1(A,B,C,D,E)
The following rules are weakly oriented:
[A >= 0] ==>
selectOrd(A,B,C,D,E) = 2
>= 2
= m4(A,B,C,D,E)
[A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] ==>
m0(A,B,C,D,E) = 0
>= 0
= m1(A,B,C,F,E)
[A >= 2 + F && 2 + F >= A] ==>
m2(A,B,C,D,E) = 1
>= 1
= m3(A,F,C,D,E)
[B >= 1 + C && A >= 2 + B && D >= E] ==>
m6(A,B,C,D,E) = 0
>= 0
= m7(A,B,C,D,E)
[D >= 1 + B && A >= 2 + C] ==>
n0(A,B,C,D,E) = 0
>= 0
= m7(A,C,C,D,E)
[B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] ==>
m7(A,B,C,D,E) = 0
>= 0
= m0(A,F,C,D,E)
[A >= 0] ==>
n1(A,B,C,D,E) = 1
>= 1
= c2(m5(A,B,0,D,E),m2(A,B,0,D,E))
[B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] ==>
n2(A,B,C,D,E) = 0
>= 0
= n3(A,B,C,F,G)
True ==>
n3(A,B,C,D,E) = 0
>= 0
= m6(A,B,C,D,E)
True ==>
n3(A,B,C,D,E) = 0
>= 0
= n0(A,D,B,E,E)
True ==>
m1(A,B,C,D,E) = 0
>= 0
= n2(A,B,C,D,E)
True ==>
n40(A,B,C,D,E) = 1
>= 1
= m2(A,B,C,D,E)
True ==>
n41(A,B,C,D,E) = 0
>= 0
= m0(A,D,B,D,E)
[A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] ==>
n4(A,B,C,D,E) = 1
>= 1
= c2(n40(A,C,F,G,E),n41(A,C,F,G,E))
True ==>
m3(A,B,C,D,E) = 1
>= 1
= n4(A,B,C,D,E)
* Step 5: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. selectOrd(A,B,C,D,E) -> m4(A,B,C,D,E) [A >= 0] (1,1)
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (?,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[0->{7},1->{11},2->{16},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},13->{2}
,14->{1},15->{13,14},16->{15}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, D) (< 7,0,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. selectOrd(A,B,C,D,E) -> m4(A,B,C,D,E) [A >= 0] (1,1)
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[0->{7},1->{11},2->{16},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},13->{2}
,14->{1},15->{13,14},16->{15}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E)
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, D) (< 7,0,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
+ Applied Processor:
ChainProcessor False [0,1,2,3,4,5,6,7,8,9,10,11,13,14,15,16]
+ Details:
We chained rule 0 to obtain the rules [17] .
* Step 7: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
7. m4(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[1->{11},2->{16},3->{5},4->{5},5->{1},6->{2},7->{6},8->{9,10},9->{3},10->{4},11->{8},13->{2},14->{1}
,15->{13,14},16->{15},17->{6}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, D) (< 7,0,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [7]
* Step 8: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
1. m0(A,B,C,D,E) -> m1(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,1)
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[1->{11},2->{16},3->{5},4->{5},5->{1},6->{2},8->{9,10},9->{3},10->{4},11->{8},13->{2},14->{1},15->{13,14}
,16->{15},17->{6}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, 1 + A) (< 1,0,E>, ?)
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
+ Applied Processor:
ChainProcessor False [1,2,3,4,5,6,8,9,10,11,13,14,15,16,17]
+ Details:
We chained rule 1 to obtain the rules [18] .
* Step 9: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
11. m1(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[2->{16},3->{5},4->{5},5->{18},6->{2},8->{9,10},9->{3},10->{4},11->{8},13->{2},14->{18},15->{13,14}
,16->{15},17->{6},18->{8}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, ?) (<11,0,D>, 1 + A) (<11,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [11]
* Step 10: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
2. m2(A,B,C,D,E) -> m3(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,1)
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[2->{16},3->{5},4->{5},5->{18},6->{2},8->{9,10},9->{3},10->{4},13->{2},14->{18},15->{13,14},16->{15}
,17->{6},18->{8}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, 2 + A) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, E)
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
+ Applied Processor:
ChainProcessor False [2,3,4,5,6,8,9,10,13,14,15,16,17,18]
+ Details:
We chained rule 2 to obtain the rules [19] .
* Step 11: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
16. m3(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[3->{5},4->{5},5->{18},6->{19},8->{9,10},9->{3},10->{4},13->{19},14->{18},15->{13,14},16->{15},17->{6}
,18->{8},19->{15}]
Sizebounds:
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<16,0,A>, A) (<16,0,B>, 2 + A) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [16]
* Step 12: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
3. m6(A,B,C,D,E) -> m7(A,B,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E] (?,1)
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[3->{5},4->{5},5->{18},6->{19},8->{9,10},9->{3},10->{4},13->{19},14->{18},15->{13,14},17->{6},18->{8}
,19->{15}]
Sizebounds:
(< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, 1 + A) (< 3,0,D>, ?) (< 3,0,E>, ?)
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
+ Applied Processor:
ChainProcessor False [3,4,5,6,8,9,10,13,14,15,17,18,19]
+ Details:
We chained rule 3 to obtain the rules [20] .
* Step 13: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
4. n0(A,B,C,D,E) -> m7(A,C,C,D,E) [D >= 1 + B && A >= 2 + C] (?,1)
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[4->{5},5->{18},6->{19},8->{9,10},9->{20},10->{4},13->{19},14->{18},15->{13,14},17->{6},18->{8},19->{15}
,20->{18}]
Sizebounds:
(< 4,0,A>, A) (< 4,0,B>, 1) (< 4,0,C>, 1 + A) (< 4,0,D>, ?) (< 4,0,E>, ?)
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
+ Applied Processor:
ChainProcessor False [4,5,6,8,9,10,13,14,15,17,18,19,20]
+ Details:
We chained rule 4 to obtain the rules [21] .
* Step 14: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
5. m7(A,B,C,D,E) -> m0(A,F,C,D,E) [B >= C && A >= 2 + B && 1 + B >= F && F >= 1 + B] (?,1)
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[5->{18},6->{19},8->{9,10},9->{20},10->{21},13->{19},14->{18},15->{13,14},17->{6},18->{8},19->{15}
,20->{18},21->{18}]
Sizebounds:
(< 5,0,A>, A) (< 5,0,B>, 1) (< 5,0,C>, 1 + A) (< 5,0,D>, ?) (< 5,0,E>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [5]
* Step 15: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
6. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),m2(A,B,0,D,E)) [A >= 0] (2,1)
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[6->{19},8->{9,10},9->{20},10->{21},13->{19},14->{18},15->{13,14},17->{6},18->{8},19->{15},20->{18}
,21->{18}]
Sizebounds:
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, 0) (< 6,0,D>, D) (< 6,0,E>, E)
(< 6,1,A>, A) (< 6,1,B>, B) (< 6,1,C>, 0) (< 6,1,D>, D) (< 6,1,E>, E)
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
+ Applied Processor:
ChainProcessor False [6,8,9,10,13,14,15,17,18,19,20,21]
+ Details:
We chained rule 6 to obtain the rules [22] .
* Step 16: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
8. n2(A,B,C,D,E) -> n3(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,1)
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[8->{9,10},9->{20},10->{21},13->{19},14->{18},15->{13,14},17->{22},18->{8},19->{15},20->{18},21->{18}
,22->{15}]
Sizebounds:
(< 8,0,A>, A) (< 8,0,B>, 1 + A) (< 8,0,C>, A) (< 8,0,D>, ?) (< 8,0,E>, ?)
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
+ Applied Processor:
ChainProcessor False [8,9,10,13,14,15,17,18,19,20,21,22]
+ Details:
We chained rule 8 to obtain the rules [23,24] .
* Step 17: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
9. n3(A,B,C,D,E) -> m6(A,B,C,D,E) True (?,1)
10. n3(A,B,C,D,E) -> n0(A,D,B,E,E) True (?,1)
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[9->{20},10->{21},13->{19},14->{18},15->{13,14},17->{22},18->{23,24},19->{15},20->{18},21->{18},22->{15}
,23->{20},24->{21}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, A) (< 9,0,D>, ?) (< 9,0,E>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, 1 + A) (<10,0,D>, ?) (<10,0,E>, ?)
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [9,10]
* Step 18: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
13. n40(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1)
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[13->{19},14->{18},15->{13,14},17->{22},18->{23,24},19->{15},20->{18},21->{18},22->{15},23->{20},24->{21}]
Sizebounds:
(<13,0,A>, A) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, E)
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
+ Applied Processor:
ChainProcessor False [13,14,15,17,18,19,20,21,22,23,24]
+ Details:
We chained rule 13 to obtain the rules [25] .
* Step 19: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
19. m2(A,B,C,D,E) -> n4(A,F,C,D,E) [A >= 2 + F && 2 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
25. n40(A,B,C,D,E) -> n4(A,F$,C,D,E) [A >= 2 + F$ && 2 + F$ >= A] (?,3)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[14->{18},15->{14,25},17->{22},18->{23,24},19->{15},20->{18},21->{18},22->{15},23->{20},24->{21},25->{15}]
Sizebounds:
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<19,0,A>, A) (<19,0,B>, 2 + A) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<25,0,A>, A) (<25,0,B>, 2 + A) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, E)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [19]
* Step 20: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
14. n41(A,B,C,D,E) -> m0(A,D,B,D,E) True (?,1)
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
25. n40(A,B,C,D,E) -> n4(A,F$,C,D,E) [A >= 2 + F$ && 2 + F$ >= A] (?,3)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[14->{18},15->{14,25},17->{22},18->{23,24},20->{18},21->{18},22->{15},23->{20},24->{21},25->{15}]
Sizebounds:
(<14,0,A>, A) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, E)
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<25,0,A>, A) (<25,0,B>, 2 + A) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, E)
+ Applied Processor:
ChainProcessor False [14,15,17,18,20,21,22,23,24,25]
+ Details:
We chained rule 14 to obtain the rules [26] .
* Step 21: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
15. n4(A,B,C,D,E) -> c2(n40(A,C,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G && 1 + C >= G && G >= 1 + C && F >= G && G >= F && A >= 2 + B && 2 + B >= A] (?,1)
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
25. n40(A,B,C,D,E) -> n4(A,F$,C,D,E) [A >= 2 + F$ && 2 + F$ >= A] (?,3)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[15->{25,26},17->{22},18->{23,24},20->{18},21->{18},22->{15},23->{20},24->{21},25->{15},26->{23,24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, E)
(<15,1,A>, A) (<15,1,B>, ?) (<15,1,C>, ?) (<15,1,D>, ?) (<15,1,E>, E)
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<25,0,A>, A) (<25,0,B>, 2 + A) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, E)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
+ Applied Processor:
ChainProcessor False [15,17,18,20,21,22,23,24,25,26]
+ Details:
We chained rule 15 to obtain the rules [27] .
* Step 22: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
25. n40(A,B,C,D,E) -> n4(A,F$,C,D,E) [A >= 2 + F$ && 2 + F$ >= A] (?,3)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},18->{23,24},20->{18},21->{18},22->{27},23->{20},24->{21},25->{27},26->{23,24},27->{26,27}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<25,0,A>, A) (<25,0,B>, 2 + A) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, E)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [25]
* Step 23: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
18. m0(A,B,C,D,E) -> n2(A,B,C,F,E) [A >= 1 + B && B >= 1 + C && A >= 1 + F && 1 + F >= A] (?,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},18->{23,24},20->{18},21->{18},22->{27},23->{20},24->{21},26->{23,24},27->{26,27}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, ?) (<18,0,D>, 1 + A) (<18,0,E>, ?)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
+ Applied Processor:
ChainProcessor False [17,18,20,21,22,23,24,26,27]
+ Details:
We chained rule 18 to obtain the rules [28,29] .
* Step 24: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
20. m6(A,B,C,D,E) -> m0(A,F$,C,D,E) [B >= 1 + C && A >= 2 + B && D >= E && B >= C && A >= 2 + B && 1 + B >= F$ && F$ >= 1 + B] (?,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
28. m0(A,B,C,D,E) -> m6(A,B,C,F$,G$) [A >= 1 + B (?,4)
&& B >= 1 + C
&& A >= 1 + F
&& 1 + F >= A
&& B >= 1 + C
&& A >= 2 + B
&& A >= 1 + F
&& 1 + F >= A]
29. m0(A,B,C,D,E) -> n0(A,F$,B,G$,G$) [A >= 1 + B (?,4)
&& B >= 1 + C
&& A >= 1 + F
&& 1 + F >= A
&& B >= 1 + C
&& A >= 2 + B
&& A >= 1 + F
&& 1 + F >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},20->{28,29},21->{28,29},22->{27},23->{20},24->{21},26->{23,24},27->{26,27},28->{20},29->{21}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<20,0,A>, A) (<20,0,B>, 1) (<20,0,C>, 1 + A) (<20,0,D>, ?) (<20,0,E>, ?)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
(<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, A) (<28,0,D>, ?) (<28,0,E>, ?)
(<29,0,A>, A) (<29,0,B>, ?) (<29,0,C>, 1 + A) (<29,0,D>, ?) (<29,0,E>, ?)
+ Applied Processor:
ChainProcessor False [17,20,21,22,23,24,26,27,28,29]
+ Details:
We chained rule 20 to obtain the rules [30,31] .
* Step 25: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
21. n0(A,B,C,D,E) -> m0(A,F$,C,D,E) [D >= 1 + B && A >= 2 + C && C >= C && A >= 2 + C && 1 + C >= F$ && F$ >= 1 + C] (?,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
28. m0(A,B,C,D,E) -> m6(A,B,C,F$,G$) [A >= 1 + B (?,4)
&& B >= 1 + C
&& A >= 1 + F
&& 1 + F >= A
&& B >= 1 + C
&& A >= 2 + B
&& A >= 1 + F
&& 1 + F >= A]
29. m0(A,B,C,D,E) -> n0(A,F$,B,G$,G$) [A >= 1 + B (?,4)
&& B >= 1 + C
&& A >= 1 + F
&& 1 + F >= A
&& B >= 1 + C
&& A >= 2 + B
&& A >= 1 + F
&& 1 + F >= A]
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},21->{28,29},22->{27},23->{30,31},24->{21},26->{23,24},27->{26,27},28->{30,31},29->{21},30->{30
,31},31->{21}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<21,0,A>, A) (<21,0,B>, 1) (<21,0,C>, 1 + A) (<21,0,D>, ?) (<21,0,E>, ?)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
(<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, A) (<28,0,D>, ?) (<28,0,E>, ?)
(<29,0,A>, A) (<29,0,B>, ?) (<29,0,C>, 1 + A) (<29,0,D>, ?) (<29,0,E>, ?)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
+ Applied Processor:
ChainProcessor False [17,21,22,23,24,26,27,28,29,30,31]
+ Details:
We chained rule 21 to obtain the rules [32,33] .
* Step 26: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
28. m0(A,B,C,D,E) -> m6(A,B,C,F$,G$) [A >= 1 + B (?,4)
&& B >= 1 + C
&& A >= 1 + F
&& 1 + F >= A
&& B >= 1 + C
&& A >= 2 + B
&& A >= 1 + F
&& 1 + F >= A]
29. m0(A,B,C,D,E) -> n0(A,F$,B,G$,G$) [A >= 1 + B (?,4)
&& B >= 1 + C
&& A >= 1 + F
&& 1 + F >= A
&& B >= 1 + C
&& A >= 2 + B
&& A >= 1 + F
&& 1 + F >= A]
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{27},23->{30,31},24->{32,33},26->{23,24},27->{26,27},28->{30,31},29->{32,33},30->{30,31}
,31->{32,33},32->{30,31},33->{32,33}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
(<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, A) (<28,0,D>, ?) (<28,0,E>, ?)
(<29,0,A>, A) (<29,0,B>, ?) (<29,0,C>, 1 + A) (<29,0,D>, ?) (<29,0,E>, ?)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [28,29]
* Step 27: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
26. n41(A,B,C,D,E) -> n2(A,D,B,F$,E) [A >= 1 + D && D >= 1 + B && A >= 1 + F$ && 1 + F$ >= A] (?,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{27},23->{30,31},24->{32,33},26->{23,24},27->{26,27},30->{30,31},31->{32,33},32->{30,31}
,33->{32,33}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, ?) (<26,0,D>, 1 + A) (<26,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
+ Applied Processor:
ChainProcessor False [17,22,23,24,26,27,30,31,32,33]
+ Details:
We chained rule 26 to obtain the rules [34,35] .
* Step 28: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
23. n2(A,B,C,D,E) -> m6(A,B,C,F,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
24. n2(A,B,C,D,E) -> n0(A,F,B,G,G) [B >= 1 + C && A >= 2 + B && A >= 1 + D && 1 + D >= A] (?,2)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
34. n41(A,B,C,D,E) -> m6(A,D,B,F$$,G$$) [A >= 1 + D (?,5)
&& D >= 1 + B
&& A >= 1 + F$
&& 1 + F$ >= A
&& D >= 1 + B
&& A >= 2 + D
&& A >= 1 + F$
&& 1 + F$ >= A]
35. n41(A,B,C,D,E) -> n0(A,F$$,D,G$$,G$$) [A >= 1 + D (?,5)
&& D >= 1 + B
&& A >= 1 + F$
&& 1 + F$ >= A
&& D >= 1 + B
&& A >= 2 + D
&& A >= 1 + F$
&& 1 + F$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{27},23->{30,31},24->{32,33},27->{27,34,35},30->{30,31},31->{32,33},32->{30,31},33->{32,33}
,34->{30,31},35->{32,33}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<23,0,A>, A) (<23,0,B>, 1 + A) (<23,0,C>, A) (<23,0,D>, ?) (<23,0,E>, ?)
(<24,0,A>, A) (<24,0,B>, ?) (<24,0,C>, 1 + A) (<24,0,D>, ?) (<24,0,E>, ?)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
(<34,0,A>, A) (<34,0,B>, 1 + A) (<34,0,C>, A) (<34,0,D>, ?) (<34,0,E>, ?)
(<35,0,A>, A) (<35,0,B>, ?) (<35,0,C>, 1 + A) (<35,0,D>, ?) (<35,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [23,24]
* Step 29: ChainProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
27. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n41(A,C,F,G,E)) [A >= 2 + G (?,4)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A]
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
34. n41(A,B,C,D,E) -> m6(A,D,B,F$$,G$$) [A >= 1 + D (?,5)
&& D >= 1 + B
&& A >= 1 + F$
&& 1 + F$ >= A
&& D >= 1 + B
&& A >= 2 + D
&& A >= 1 + F$
&& 1 + F$ >= A]
35. n41(A,B,C,D,E) -> n0(A,F$$,D,G$$,G$$) [A >= 1 + D (?,5)
&& D >= 1 + B
&& A >= 1 + F$
&& 1 + F$ >= A
&& D >= 1 + B
&& A >= 2 + D
&& A >= 1 + F$
&& 1 + F$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{27},27->{27,34,35},30->{30,31},31->{32,33},32->{30,31},33->{32,33},34->{30,31},35->{32,33}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<27,0,A>, A) (<27,0,B>, 2 + A) (<27,0,C>, ?) (<27,0,D>, ?) (<27,0,E>, E)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
(<34,0,A>, A) (<34,0,B>, 1 + A) (<34,0,C>, A) (<34,0,D>, ?) (<34,0,E>, ?)
(<35,0,A>, A) (<35,0,B>, ?) (<35,0,C>, 1 + A) (<35,0,D>, ?) (<35,0,E>, ?)
+ Applied Processor:
ChainProcessor False [17,22,27,30,31,32,33,34,35]
+ Details:
We chained rule 27 to obtain the rules [36,37] .
* Step 30: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
34. n41(A,B,C,D,E) -> m6(A,D,B,F$$,G$$) [A >= 1 + D (?,5)
&& D >= 1 + B
&& A >= 1 + F$
&& 1 + F$ >= A
&& D >= 1 + B
&& A >= 2 + D
&& A >= 1 + F$
&& 1 + F$ >= A]
35. n41(A,B,C,D,E) -> n0(A,F$$,D,G$$,G$$) [A >= 1 + D (?,5)
&& D >= 1 + B
&& A >= 1 + F$
&& 1 + F$ >= A
&& D >= 1 + B
&& A >= 2 + D
&& A >= 1 + F$
&& 1 + F$ >= A]
36. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),m6(A,G,F$$,F$$$$,G$$$$)) [A >= 2 + G (?,9)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A
&& A >= 1 + G
&& G >= 1 + F$$
&& A >= 1 + F$$$
&& 1 + F$$$ >= A
&& G >= 1 + F$$
&& A >= 2 + G
&& A >= 1 + F$$$
&& 1 + F$$$ >= A]
37. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n0(A,F$$$$,G,G$$$$,G$$$$)) [A >= 2 + G (?,9)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A
&& A >= 1 + G
&& G >= 1 + F$$
&& A >= 1 + F$$$
&& 1 + F$$$ >= A
&& G >= 1 + F$$
&& A >= 2 + G
&& A >= 1 + F$$$
&& 1 + F$$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{36,37},30->{30,31},31->{32,33},32->{30,31},33->{32,33},34->{30,31},35->{32,33},36->{30,31
,36,37},37->{32,33,36,37}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
(<34,0,A>, A) (<34,0,B>, 1 + A) (<34,0,C>, A) (<34,0,D>, ?) (<34,0,E>, ?)
(<35,0,A>, A) (<35,0,B>, ?) (<35,0,C>, 1 + A) (<35,0,D>, ?) (<35,0,E>, ?)
(<36,0,A>, A) (<36,0,B>, 1 + A) (<36,0,C>, A) (<36,0,D>, ?) (<36,0,E>, ?)
(<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 1 + A) (<37,0,D>, ?) (<37,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [34,35]
* Step 31: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
36. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),m6(A,G,F$$,F$$$$,G$$$$)) [A >= 2 + G (?,9)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A
&& A >= 1 + G
&& G >= 1 + F$$
&& A >= 1 + F$$$
&& 1 + F$$$ >= A
&& G >= 1 + F$$
&& A >= 2 + G
&& A >= 1 + F$$$
&& 1 + F$$$ >= A]
37. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n0(A,F$$$$,G,G$$$$,G$$$$)) [A >= 2 + G (?,9)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A
&& A >= 1 + G
&& G >= 1 + F$$
&& A >= 1 + F$$$
&& 1 + F$$$ >= A
&& G >= 1 + F$$
&& A >= 2 + G
&& A >= 1 + F$$$
&& 1 + F$$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{36,37},30->{30,31},31->{32,33},32->{30,31},33->{32,33},36->{30,31,36,37},37->{32,33,36,37}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
(<36,0,A>, A) (<36,0,B>, 1 + A) (<36,0,C>, A) (<36,0,D>, ?) (<36,0,E>, ?)
(<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 1 + A) (<37,0,D>, ?) (<37,0,E>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(22,36)
,(22,37)
,(36,30)
,(36,31)
,(36,36)
,(36,37)
,(37,32)
,(37,33)
,(37,36)
,(37,37)]
* Step 32: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
30. m6(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
31. m6(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [B >= 1 + C (?,6)
&& A >= 2 + B
&& D >= E
&& B >= C
&& A >= 2 + B
&& 1 + B >= F$
&& F$ >= 1 + B
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
32. n0(A,B,C,D,E) -> m6(A,F$,C,F$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
33. n0(A,B,C,D,E) -> n0(A,F$$$,F$,G$$$,G$$$) [D >= 1 + B (?,6)
&& A >= 2 + C
&& C >= C
&& A >= 2 + C
&& 1 + C >= F$
&& F$ >= 1 + C
&& A >= 1 + F$
&& F$ >= 1 + C
&& A >= 1 + F$$
&& 1 + F$$ >= A
&& F$ >= 1 + C
&& A >= 2 + F$
&& A >= 1 + F$$
&& 1 + F$$ >= A]
36. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),m6(A,G,F$$,F$$$$,G$$$$)) [A >= 2 + G (?,9)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A
&& A >= 1 + G
&& G >= 1 + F$$
&& A >= 1 + F$$$
&& 1 + F$$$ >= A
&& G >= 1 + F$$
&& A >= 2 + G
&& A >= 1 + F$$$
&& 1 + F$$$ >= A]
37. n4(A,B,C,D,E) -> c2(n4(A,F$$,F,G,E),n0(A,F$$$$,G,G$$$$,G$$$$)) [A >= 2 + G (?,9)
&& 1 + C >= G
&& G >= 1 + C
&& F >= G
&& G >= F
&& A >= 2 + B
&& 2 + B >= A
&& A >= 2 + F$$
&& 2 + F$$ >= A
&& A >= 1 + G
&& G >= 1 + F$$
&& A >= 1 + F$$$
&& 1 + F$$$ >= A
&& G >= 1 + F$$
&& A >= 2 + G
&& A >= 1 + F$$$
&& 1 + F$$$ >= A]
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{},30->{30,31},31->{32,33},32->{30,31},33->{32,33},36->{},37->{}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
(<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, A) (<30,0,D>, ?) (<30,0,E>, ?)
(<31,0,A>, A) (<31,0,B>, ?) (<31,0,C>, 1 + A) (<31,0,D>, ?) (<31,0,E>, ?)
(<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, A) (<32,0,D>, ?) (<32,0,E>, ?)
(<33,0,A>, A) (<33,0,B>, ?) (<33,0,C>, 1 + A) (<33,0,D>, ?) (<33,0,E>, ?)
(<36,0,A>, A) (<36,0,B>, 1 + A) (<36,0,C>, A) (<36,0,D>, ?) (<36,0,E>, ?)
(<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 1 + A) (<37,0,D>, ?) (<37,0,E>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [30,31,32,33,36,37]
* Step 33: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
17. selectOrd(A,B,C,D,E) -> n1(A,B,C,D,E) [A >= 0 && A >= 0] (1,2)
22. n1(A,B,C,D,E) -> c2(m5(A,B,0,D,E),n4(A,F$,0,D,E)) [A >= 0 && A >= 2 + F$ && 2 + F$ >= A] (2,3)
Signature:
{(m0,5)
;(m1,5)
;(m2,5)
;(m3,5)
;(m4,5)
;(m5,5)
;(m6,5)
;(m7,5)
;(m8,5)
;(m9,5)
;(n0,5)
;(n1,5)
;(n2,5)
;(n3,5)
;(n4,5)
;(n40,5)
;(n41,5)
;(selectOrd,5)}
Flow Graph:
[17->{22},22->{}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, C) (<17,0,D>, D) (<17,0,E>, E)
(<22,0,A>, A) (<22,0,B>, 2 + A) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, E)
+ Applied Processor:
LeafRules
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))