WORST_CASE(?,O(n^1))
* Step 1: UnsatRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
1. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [1 >= A] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [1 >= A] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
13. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,11 + C,C,D) [C >= 101 && 100 >= C] (?,1)
14. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,1 + C,C,D) [100 >= C && C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) True (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{1,2},1->{16},2->{3,4},3->{5},4->{6,7},5->{3,4},6->{8,9,10,11},7->{16},8->{12,13,14,15},9->{12,13,14
,15},10->{12,13,14,15},11->{6,7},12->{6,7},13->{6,7},14->{6,7},15->{6,7},16->{}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [13,14]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
1. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [1 >= A] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [1 >= A] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) True (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{1,2},1->{16},2->{3,4},3->{5},4->{6,7},5->{3,4},6->{8,9,10,11},7->{16},8->{12,15},9->{12,15},10->{12
,15},11->{6,7},12->{6,7},15->{6,7},16->{}]
+ 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)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, D, .= 0)
(< 2,0,A>, 1, .= 1) (< 2,0,B>, A, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0)
(< 5,0,A>, 1 + A, .+ 1) (< 5,0,B>, 11 + B, .+ 11) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, 10 + B, .+ 10) (< 8,0,D>, 1 + A, .+ 1)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, 10 + B, .+ 10) (< 9,0,D>, 1 + A, .+ 1)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, 10 + B, .+ 10) (<10,0,D>, 1 + A, .+ 1)
(<11,0,A>, 1, .= 1) (<11,0,B>, 10 + B, .+ 10) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0)
(<12,0,A>, D, .= 0) (<12,0,B>, 1 + C, .+ 1) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0)
(<15,0,A>, 1 + D, .+ 1) (<15,0,B>, 11 + C, .+ 11) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
1. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [1 >= A] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [1 >= A] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) True (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{1,2},1->{16},2->{3,4},3->{5},4->{6,7},5->{3,4},6->{8,9,10,11},7->{16},8->{12,15},9->{12,15},10->{12
,15},11->{6,7},12->{6,7},15->{6,7},16->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, 1) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
* Step 4: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
1. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [1 >= A] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [1 >= A] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) True (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{1,2},1->{16},2->{3,4},3->{5},4->{6,7},5->{3,4},6->{8,9,10,11},7->{16},8->{12,15},9->{12,15},10->{12
,15},11->{6,7},12->{6,7},15->{6,7},16->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, 1) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(2,4),(6,9),(8,12),(11,6)]
* Step 5: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
1. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [1 >= A] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [1 >= A] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) True (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{1,2},1->{16},2->{3},3->{5},4->{6,7},5->{3,4},6->{8,10,11},7->{16},8->{15},9->{12,15},10->{12,15}
,11->{7},12->{6,7},15->{6,7},16->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, 1) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [9]
* Step 6: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
1. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [1 >= A] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) True (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{1,2},1->{16},2->{3},3->{5},4->{6,7},5->{3,4},6->{8,10,11},7->{16},8->{15},10->{12,15},11->{7},12->{6
,7},15->{6,7},16->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, 1) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [11,1,7,16]
* Step 7: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (?,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{2},2->{3},3->{5},4->{6},5->{3,4},6->{8,10},8->{15},10->{12,15},12->{6},15->{6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalsipma91bb11in) = 1
p(evalsipma91bb2in) = 2
p(evalsipma91bb3in) = 2
p(evalsipma91bb5in) = 1
p(evalsipma91bb8in) = 1
p(evalsipma91entryin) = 2
p(evalsipma91start) = 2
The following rules are strictly oriented:
[B >= 101] ==>
evalsipma91bb3in(A,B,C,D) = 2
> 1
= evalsipma91bb11in(A,B,C,D)
The following rules are weakly oriented:
True ==>
evalsipma91start(A,B,C,D) = 2
>= 2
= evalsipma91entryin(A,B,C,D)
[100 >= A] ==>
evalsipma91entryin(A,B,C,D) = 2
>= 2
= evalsipma91bb3in(1,A,C,D)
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 2
>= 2
= evalsipma91bb2in(A,B,C,D)
True ==>
evalsipma91bb2in(A,B,C,D) = 2
>= 2
= evalsipma91bb3in(1 + A,11 + B,C,D)
[A >= 2] ==>
evalsipma91bb11in(A,B,C,D) = 1
>= 1
= evalsipma91bb5in(A,B,C,D)
[110 >= B] ==>
evalsipma91bb5in(A,B,C,D) = 1
>= 1
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[A >= 3] ==>
evalsipma91bb5in(A,B,C,D) = 1
>= 1
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[C >= 101] ==>
evalsipma91bb8in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(D,1 + C,C,D)
[100 >= C] ==>
evalsipma91bb8in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(1 + D,11 + C,C,D)
* Step 8: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{2},2->{3},3->{5},4->{6},5->{3,4},6->{8,10},8->{15},10->{12,15},12->{6},15->{6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (?,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{2},2->{3},3->{5},4->{6},5->{3,4},6->{8,10},8->{15},10->{12,15},12->{6},15->{6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [3,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalsipma91bb2in) = 100 + -1*x2
p(evalsipma91bb3in) = 101 + -1*x2
The following rules are strictly oriented:
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 101 + -1*B
> 100 + -1*B
= evalsipma91bb2in(A,B,C,D)
The following rules are weakly oriented:
True ==>
evalsipma91bb2in(A,B,C,D) = 100 + -1*B
>= 90 + -1*B
= evalsipma91bb3in(1 + A,11 + B,C,D)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
* Step 10: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (101 + A,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (?,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{2},2->{3},3->{5},4->{6},5->{3,4},6->{8,10},8->{15},10->{12,15},12->{6},15->{6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1)
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (101 + A,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (101 + A,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[0->{2},2->{3},3->{5},4->{6},5->{3,4},6->{8,10},8->{15},10->{12,15},12->{6},15->{6}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
+ Applied Processor:
ChainProcessor False [0,2,3,4,5,6,8,10,12,15]
+ Details:
We chained rule 0 to obtain the rules [16] .
* Step 12: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,1)
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (101 + A,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (101 + A,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[2->{3,4},3->{5},4->{6},5->{3,4},6->{8,10},8->{12,15},10->{12,15},12->{6},15->{6},16->{3,4}]
Sizebounds:
(< 2,0,A>, 1) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [2]
* Step 13: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [100 >= B] (101 + A,1)
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (101 + A,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[3->{5},4->{6},5->{3,4},6->{8,10},8->{12,15},10->{12,15},12->{6},15->{6},16->{3,4}]
Sizebounds:
(< 3,0,A>, ?) (< 3,0,B>, 100) (< 3,0,C>, C) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
ChainProcessor False [3,4,5,6,8,10,12,15,16]
+ Details:
We chained rule 3 to obtain the rules [17] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) True (101 + A,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[4->{6},5->{4,17},6->{8,10},8->{12,15},10->{12,15},12->{6},15->{6},16->{4,17},17->{4,17}]
Sizebounds:
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, 100) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [5]
* Step 15: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
4. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [B >= 101] (2,1)
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[4->{6},6->{8,10},8->{12,15},10->{12,15},12->{6},15->{6},16->{4,17},17->{4,17}]
Sizebounds:
(< 4,0,A>, ?) (< 4,0,B>, 100 + A) (< 4,0,C>, C) (< 4,0,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
+ Applied Processor:
ChainProcessor False [4,6,8,10,12,15,16,17]
+ Details:
We chained rule 4 to obtain the rules [18] .
* Step 16: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
6. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [A >= 2] (?,1)
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
18. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [B >= 101 && A >= 2] (2,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[6->{8,10},8->{12,15},10->{12,15},12->{6},15->{6},16->{17,18},17->{17,18},18->{8,10}]
Sizebounds:
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
+ Applied Processor:
ChainProcessor False [6,8,10,12,15,16,17,18]
+ Details:
We chained rule 6 to obtain the rules [19,20] .
* Step 17: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
8. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [110 >= B] (?,1)
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
18. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [B >= 101 && A >= 2] (2,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[8->{12,15},10->{12,15},12->{19,20},15->{19,20},16->{17,18},17->{17,18},18->{8,10},19->{12,15},20->{12
,15}]
Sizebounds:
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
+ Applied Processor:
ChainProcessor False [8,10,12,15,16,17,18,19,20]
+ Details:
We chained rule 8 to obtain the rules [21,22] .
* Step 18: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 3] (?,1)
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
18. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [B >= 101 && A >= 2] (2,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
21. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [110 >= B && -10 + B >= 101] (?,2)
22. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [110 >= B && 100 >= -10 + B] (?,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[10->{12,15},12->{19,20},15->{19,20},16->{17,18},17->{17,18},18->{10,21,22},19->{12,15},20->{12,15}
,21->{19,20},22->{19,20}]
Sizebounds:
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
+ Applied Processor:
ChainProcessor False [10,12,15,16,17,18,19,20,21,22]
+ Details:
We chained rule 10 to obtain the rules [23,24] .
* Step 19: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [C >= 101] (?,1)
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
18. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [B >= 101 && A >= 2] (2,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
21. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [110 >= B && -10 + B >= 101] (?,2)
22. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [110 >= B && 100 >= -10 + B] (?,2)
23. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [A >= 3 && -10 + B >= 101] (?,2)
24. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [A >= 3 && 100 >= -10 + B] (?,2)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[12->{19,20},15->{19,20},16->{17,18},17->{17,18},18->{21,22,23,24},19->{12,15},20->{12,15},21->{19,20}
,22->{19,20},23->{19,20},24->{19,20}]
Sizebounds:
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?)
+ Applied Processor:
ChainProcessor False [12,15,16,17,18,19,20,21,22,23,24]
+ Details:
We chained rule 12 to obtain the rules [25,26] .
* Step 20: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
15. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [100 >= C] (?,1)
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
18. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [B >= 101 && A >= 2] (2,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
21. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [110 >= B && -10 + B >= 101] (?,2)
22. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [110 >= B && 100 >= -10 + B] (?,2)
23. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [A >= 3 && -10 + B >= 101] (?,2)
24. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [A >= 3 && 100 >= -10 + B] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[15->{19,20},16->{17,18},17->{17,18},18->{21,22,23,24},19->{15,25,26},20->{15,25,26},21->{19,20},22->{19
,20},23->{19,20},24->{19,20},25->{15,25,26},26->{15,25,26}]
Sizebounds:
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
+ Applied Processor:
ChainProcessor False [15,16,17,18,19,20,21,22,23,24,25,26]
+ Details:
We chained rule 15 to obtain the rules [27,28] .
* Step 21: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
18. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [B >= 101 && A >= 2] (2,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
21. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [110 >= B && -10 + B >= 101] (?,2)
22. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [110 >= B && 100 >= -10 + B] (?,2)
23. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [A >= 3 && -10 + B >= 101] (?,2)
24. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [A >= 3 && 100 >= -10 + B] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17,18},17->{17,18},18->{21,22,23,24},19->{25,26,27,28},20->{25,26,27,28},21->{19,20},22->{19,20}
,23->{19,20},24->{19,20},25->{25,26,27,28},26->{25,26,27,28},27->{25,26,27,28},28->{25,26,27,28}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
+ Applied Processor:
ChainProcessor False [16,17,18,19,20,21,22,23,24,25,26,27,28]
+ Details:
We chained rule 18 to obtain the rules [29,30,31,32] .
* Step 22: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
21. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [110 >= B && -10 + B >= 101] (?,2)
22. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [110 >= B && 100 >= -10 + B] (?,2)
23. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [A >= 3 && -10 + B >= 101] (?,2)
24. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [A >= 3 && 100 >= -10 + B] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
29. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && -10 + B >= 101] (2,4)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17,29,30,31,32},17->{17,29,30,31,32},19->{25,26,27,28},20->{25,26,27,28},21->{19,20},22->{19,20}
,23->{19,20},24->{19,20},25->{25,26,27,28},26->{25,26,27,28},27->{25,26,27,28},28->{25,26,27,28},29->{19,20}
,30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?) (<29,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
(<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [21,22,23,24]
* Step 23: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
29. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && -10 + B >= 101] (2,4)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17,29,30,31,32},17->{17,29,30,31,32},19->{25,26,27,28},20->{25,26,27,28},25->{25,26,27,28},26->{25
,26,27,28},27->{25,26,27,28},28->{25,26,27,28},29->{19,20},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?) (<29,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
(<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?)
+ Applied Processor:
ChainProcessor False [16,17,19,20,25,26,27,28,29,30,31,32]
+ Details:
We chained rule 29 to obtain the rules [33,34] .
* Step 24: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
33. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb8in(-1 + A,-9 + B,-19 + B,-2 + A) [B >= 101 && A >= 2 && 110 >= B && -10 + B >= 101 && -1 + A >= 2 && 110 >= -9 + B] (2,6)
34. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb8in(-1 + A,-9 + B,-19 + B,-2 + A) [B >= 101 && A >= 2 && 110 >= B && -10 + B >= 101 && -1 + A >= 2 && -1 + A >= 3] (2,6)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17,30,31,32,33,34},17->{17,30,31,32,33,34},19->{25,26,27,28},20->{25,26,27,28},25->{25,26,27,28}
,26->{25,26,27,28},27->{25,26,27,28},28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20},33->{25,26,27,28}
,34->{25,26,27,28}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
(<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?)
(<33,0,A>, ?) (<33,0,B>, ?) (<33,0,C>, ?) (<33,0,D>, ?)
(<34,0,A>, ?) (<34,0,B>, ?) (<34,0,C>, ?) (<34,0,D>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(16,30)
,(16,31)
,(16,32)
,(16,33)
,(16,34)
,(17,33)
,(17,34)
,(19,25)
,(19,26)
,(25,25)
,(25,26)
,(27,25)
,(27,26)
,(33,25)
,(33,26)
,(33,27)
,(33,28)
,(34,25)
,(34,26)
,(34,27)
,(34,28)]
* Step 25: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
33. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb8in(-1 + A,-9 + B,-19 + B,-2 + A) [B >= 101 && A >= 2 && 110 >= B && -10 + B >= 101 && -1 + A >= 2 && 110 >= -9 + B] (2,6)
34. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb8in(-1 + A,-9 + B,-19 + B,-2 + A) [B >= 101 && A >= 2 && 110 >= B && -10 + B >= 101 && -1 + A >= 2 && -1 + A >= 3] (2,6)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20},33->{},34->{}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
(<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?)
(<33,0,A>, ?) (<33,0,B>, ?) (<33,0,C>, ?) (<33,0,D>, ?)
(<34,0,A>, ?) (<34,0,B>, ?) (<34,0,C>, ?) (<34,0,D>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [33,34]
* Step 26: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, ?) (<17,0,B>, 100) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
(<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<16,0,A>, 1, .= 1) (<16,0,B>, A, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0)
(<17,0,A>, 1 + A, .+ 1) (<17,0,B>, 11 + B, .+ 11) (<17,0,C>, C, .= 0) (<17,0,D>, D, .= 0)
(<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, 10 + B, .+ 10) (<19,0,D>, 1 + A, .+ 1)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, 10 + B, .+ 10) (<20,0,D>, 1 + A, .+ 1)
(<25,0,A>, D, .= 0) (<25,0,B>, 110, .= 110) (<25,0,C>, 100, .= 100) (<25,0,D>, 1 + D, .+ 1)
(<26,0,A>, D, .= 0) (<26,0,B>, 1 + C, .+ 1) (<26,0,C>, 9 + C, .+ 9) (<26,0,D>, 1 + D, .+ 1)
(<27,0,A>, 1 + D, .+ 1) (<27,0,B>, 111 + C, .+ 111) (<27,0,C>, 101 + C, .+ 101) (<27,0,D>, D, .= 0)
(<28,0,A>, 2 + D, .+ 2) (<28,0,B>, 11 + C, .+ 11) (<28,0,C>, 1 + C, .+ 1) (<28,0,D>, D, .= 0)
(<30,0,A>, A, .= 0) (<30,0,B>, 111, .= 111) (<30,0,C>, 100, .= 100) (<30,0,D>, 1 + A, .+ 1)
(<31,0,A>, 1 + A, .+ 1) (<31,0,B>, 9 + B, .+ 9) (<31,0,C>, 10 + B, .+ 10) (<31,0,D>, 1 + A, .+ 1)
(<32,0,A>, A, .= 0) (<32,0,B>, 111, .= 111) (<32,0,C>, 100, .= 100) (<32,0,D>, 1 + A, .+ 1)
* Step 27: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?) (<28,0,D>, ?)
(<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?)
(<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?)
(<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
* Step 28: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 16 : True 17 : [False] 19 : True 20 : True 25 : True 26 : True 27 : True 28 : True 30 : [False] 31 : [False] 32 : [False] .
* Step 29: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (?,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalsipma91bb11in) = 1
p(evalsipma91bb3in) = 1
p(evalsipma91bb8in) = 0
p(evalsipma91start) = 1
The following rules are strictly oriented:
[A >= 2 && A >= 3] ==>
evalsipma91bb11in(A,B,C,D) = 1
> 0
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
The following rules are weakly oriented:
[100 >= A] ==>
evalsipma91start(A,B,C,D) = 1
>= 1
= evalsipma91bb3in(1,A,C,D)
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb3in(1 + A,11 + B,C,D)
[A >= 2 && 110 >= B] ==>
evalsipma91bb11in(A,B,C,D) = 1
>= 0
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[C >= 101 && D >= 2 && 110 >= 1 + C] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[C >= 101 && D >= 2 && D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[100 >= C && 1 + D >= 2 && 110 >= 11 + C] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[100 >= C && 1 + D >= 2 && 1 + D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
* Step 30: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (?,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (1,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
+ Details:
We apply a polynomial interpretation of shape constant:
p(evalsipma91bb11in) = 1
p(evalsipma91bb3in) = 1
p(evalsipma91bb8in) = 0
p(evalsipma91start) = 1
The following rules are strictly oriented:
[A >= 2 && 110 >= B] ==>
evalsipma91bb11in(A,B,C,D) = 1
> 0
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[A >= 2 && A >= 3] ==>
evalsipma91bb11in(A,B,C,D) = 1
> 0
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
The following rules are weakly oriented:
[100 >= A] ==>
evalsipma91start(A,B,C,D) = 1
>= 1
= evalsipma91bb3in(1,A,C,D)
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb3in(1 + A,11 + B,C,D)
[C >= 101 && D >= 2 && 110 >= 1 + C] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[C >= 101 && D >= 2 && D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[100 >= C && 1 + D >= 2 && 110 >= 11 + C] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[100 >= C && 1 + D >= 2 && 1 + D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 0
>= 0
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 1
>= 1
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
* Step 31: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (1,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (1,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (?,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalsipma91bb11in) = 84 + 9*x1 + -1*x2
p(evalsipma91bb3in) = 93 + 9*x1 + -1*x2
p(evalsipma91bb8in) = 83 + -1*x3 + 9*x4
p(evalsipma91start) = 102 + -1*x1
The following rules are strictly oriented:
[100 >= C && 1 + D >= 2 && 1 + D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 83 + -1*C + 9*D
> 82 + -1*C + 9*D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
> 83 + 9*A + -1*B
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
> 83 + 9*A + -1*B
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
The following rules are weakly oriented:
[100 >= A] ==>
evalsipma91start(A,B,C,D) = 102 + -1*A
>= 102 + -1*A
= evalsipma91bb3in(1,A,C,D)
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
>= 91 + 9*A + -1*B
= evalsipma91bb3in(1 + A,11 + B,C,D)
[A >= 2 && 110 >= B] ==>
evalsipma91bb11in(A,B,C,D) = 84 + 9*A + -1*B
>= 84 + 9*A + -1*B
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[A >= 2 && A >= 3] ==>
evalsipma91bb11in(A,B,C,D) = 84 + 9*A + -1*B
>= 84 + 9*A + -1*B
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[C >= 101 && D >= 2 && 110 >= 1 + C] ==>
evalsipma91bb8in(A,B,C,D) = 83 + -1*C + 9*D
>= 83 + -1*C + 9*D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[C >= 101 && D >= 2 && D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 83 + -1*C + 9*D
>= 83 + -1*C + 9*D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[100 >= C && 1 + D >= 2 && 110 >= 11 + C] ==>
evalsipma91bb8in(A,B,C,D) = 83 + -1*C + 9*D
>= 82 + -1*C + 9*D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
>= 84 + 9*A + -1*B
= evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A)
* Step 32: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (1,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (1,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (?,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (102 + A,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalsipma91bb11in) = 92 + 9*x1 + -1*x2
p(evalsipma91bb3in) = 93 + 9*x1 + -1*x2
p(evalsipma91bb8in) = 91 + -1*x3 + 9*x4
p(evalsipma91start) = 102 + -1*x1
The following rules are strictly oriented:
[100 >= C && 1 + D >= 2 && 110 >= 11 + C] ==>
evalsipma91bb8in(A,B,C,D) = 91 + -1*C + 9*D
> 90 + -1*C + 9*D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[100 >= C && 1 + D >= 2 && 1 + D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 91 + -1*C + 9*D
> 90 + -1*C + 9*D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
> 91 + 9*A + -1*B
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
> 91 + 9*A + -1*B
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
The following rules are weakly oriented:
[100 >= A] ==>
evalsipma91start(A,B,C,D) = 102 + -1*A
>= 102 + -1*A
= evalsipma91bb3in(1,A,C,D)
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
>= 91 + 9*A + -1*B
= evalsipma91bb3in(1 + A,11 + B,C,D)
[A >= 2 && 110 >= B] ==>
evalsipma91bb11in(A,B,C,D) = 92 + 9*A + -1*B
>= 92 + 9*A + -1*B
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[A >= 2 && A >= 3] ==>
evalsipma91bb11in(A,B,C,D) = 92 + 9*A + -1*B
>= 92 + 9*A + -1*B
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[C >= 101 && D >= 2 && 110 >= 1 + C] ==>
evalsipma91bb8in(A,B,C,D) = 91 + -1*C + 9*D
>= 91 + -1*C + 9*D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[C >= 101 && D >= 2 && D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 91 + -1*C + 9*D
>= 91 + -1*C + 9*D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] ==>
evalsipma91bb3in(A,B,C,D) = 93 + 9*A + -1*B
>= 92 + 9*A + -1*B
= evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A)
* Step 33: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (1,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (1,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (?,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (102 + A,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (102 + A,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalsipma91bb11in) = 91 + 10*x1 + -1*x2
p(evalsipma91bb3in) = 90 + 10*x1 + -1*x2
p(evalsipma91bb8in) = 90 + -1*x3 + 10*x4
p(evalsipma91start) = 101 + -1*x1
The following rules are strictly oriented:
[100 >= A] ==>
evalsipma91start(A,B,C,D) = 101 + -1*A
> 100 + -1*A
= evalsipma91bb3in(1,A,C,D)
[A >= 2 && 110 >= B] ==>
evalsipma91bb11in(A,B,C,D) = 91 + 10*A + -1*B
> 90 + 10*A + -1*B
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[C >= 101 && D >= 2 && 110 >= 1 + C] ==>
evalsipma91bb8in(A,B,C,D) = 90 + -1*C + 10*D
> 89 + -1*C + 10*D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[100 >= C && 1 + D >= 2 && 110 >= 11 + C] ==>
evalsipma91bb8in(A,B,C,D) = 90 + -1*C + 10*D
> 89 + -1*C + 10*D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[100 >= C && 1 + D >= 2 && 1 + D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 90 + -1*C + 10*D
> 89 + -1*C + 10*D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
The following rules are weakly oriented:
[100 >= B] ==>
evalsipma91bb3in(A,B,C,D) = 90 + 10*A + -1*B
>= 89 + 10*A + -1*B
= evalsipma91bb3in(1 + A,11 + B,C,D)
[A >= 2 && A >= 3] ==>
evalsipma91bb11in(A,B,C,D) = 91 + 10*A + -1*B
>= 90 + 10*A + -1*B
= evalsipma91bb8in(A,B,-10 + B,-1 + A)
[C >= 101 && D >= 2 && D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = 90 + -1*C + 10*D
>= 89 + -1*C + 10*D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 90 + 10*A + -1*B
>= 90 + 10*A + -1*B
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] ==>
evalsipma91bb3in(A,B,C,D) = 90 + 10*A + -1*B
>= 90 + 10*A + -1*B
= evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A)
[B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] ==>
evalsipma91bb3in(A,B,C,D) = 90 + 10*A + -1*B
>= 90 + 10*A + -1*B
= evalsipma91bb11in(A,1 + B,-10 + B,-1 + A)
* Step 34: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (1,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (1,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (101 + A,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (?,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (101 + A,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (101 + A,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [27,25,26,28], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalsipma91bb8in) = x4
The following rules are strictly oriented:
[C >= 101 && D >= 2 && 110 >= 1 + C] ==>
evalsipma91bb8in(A,B,C,D) = D
> -1 + D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
[C >= 101 && D >= 2 && D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = D
> -1 + D
= evalsipma91bb8in(D,1 + C,-9 + C,-1 + D)
The following rules are weakly oriented:
[100 >= C && 1 + D >= 2 && 110 >= 11 + C] ==>
evalsipma91bb8in(A,B,C,D) = D
>= D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
[100 >= C && 1 + D >= 2 && 1 + D >= 3] ==>
evalsipma91bb8in(A,B,C,D) = D
>= D
= evalsipma91bb8in(1 + D,11 + C,1 + C,D)
We use the following global sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
* Step 35: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. evalsipma91start(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (1,2)
17. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 >= B] (101 + A,2)
19. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && 110 >= B] (1,2)
20. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [A >= 2 && A >= 3] (1,2)
25. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && 110 >= 1 + C] (101 + A,3)
26. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(D,1 + C,-9 + C,-1 + D) [C >= 101 && D >= 2 && D >= 3] (208 + 2*A,3)
27. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 110 >= 11 + C] (101 + A,3)
28. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb8in(1 + D,11 + C,1 + C,D) [100 >= C && 1 + D >= 2 && 1 + D >= 3] (101 + A,3)
30. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && 110 >= B && 100 >= -10 + B] (2,4)
31. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-9 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && -10 + B >= 101] (2,4)
32. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,1 + B,-10 + B,-1 + A) [B >= 101 && A >= 2 && A >= 3 && 100 >= -10 + B] (2,4)
Signature:
{(evalsipma91bb11in,4)
;(evalsipma91bb2in,4)
;(evalsipma91bb3in,4)
;(evalsipma91bb5in,4)
;(evalsipma91bb8in,4)
;(evalsipma91entryin,4)
;(evalsipma91returnin,4)
;(evalsipma91start,4)
;(evalsipma91stop,4)}
Flow Graph:
[16->{17},17->{17,30,31,32},19->{27,28},20->{25,26,27,28},25->{27,28},26->{25,26,27,28},27->{27,28}
,28->{25,26,27,28},30->{19,20},31->{19,20},32->{19,20}]
Sizebounds:
(<16,0,A>, 1) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, D)
(<17,0,A>, 102 + A) (<17,0,B>, 1111 + 12*A) (<17,0,C>, C) (<17,0,D>, D)
(<19,0,A>, 103 + A) (<19,0,B>, 1120 + 12*A) (<19,0,C>, 1130 + 12*A) (<19,0,D>, 104 + A)
(<20,0,A>, 103 + A) (<20,0,B>, 1120 + 12*A) (<20,0,C>, 1130 + 12*A) (<20,0,D>, 104 + A)
(<25,0,A>, ?) (<25,0,B>, 110) (<25,0,C>, 100) (<25,0,D>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?) (<26,0,D>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, 101) (<27,0,D>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, 101) (<28,0,D>, ?)
(<30,0,A>, 102 + A) (<30,0,B>, 111) (<30,0,C>, 100) (<30,0,D>, 103 + A)
(<31,0,A>, 103 + A) (<31,0,B>, 1120 + 12*A) (<31,0,C>, 1121 + 12*A) (<31,0,D>, 103 + A)
(<32,0,A>, 102 + A) (<32,0,B>, 111) (<32,0,C>, 100) (<32,0,D>, 103 + A)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))