diff options
author | Carlo Zancanaro <carlo@carlo-laptop> | 2012-11-28 11:09:10 +1100 |
---|---|---|
committer | Carlo Zancanaro <carlo@carlo-laptop> | 2012-11-28 11:09:10 +1100 |
commit | 62d8d7011c339f9b192099b2fc6a6d2f567f0a4d (patch) | |
tree | 13dae8f7e7de727677450535288f90b4a30ba70d /tex/thesis/implementation/experiments | |
parent | 839764bd955d2bddedb4a38ab1d4d92c797c56b9 (diff) |
Ahhh! Lots of things.
Diffstat (limited to 'tex/thesis/implementation/experiments')
-rw-r--r-- | tex/thesis/implementation/experiments/counter.c | 4 | ||||
-rw-r--r-- | tex/thesis/implementation/experiments/example-output | 90 | ||||
-rw-r--r-- | tex/thesis/implementation/experiments/example.c | 4 | ||||
-rw-r--r-- | tex/thesis/implementation/experiments/fib-output | 302 | ||||
-rw-r--r-- | tex/thesis/implementation/experiments/nested-output | 260 |
5 files changed, 139 insertions, 521 deletions
diff --git a/tex/thesis/implementation/experiments/counter.c b/tex/thesis/implementation/experiments/counter.c index ae935e6..ebd6ff0 100644 --- a/tex/thesis/implementation/experiments/counter.c +++ b/tex/thesis/implementation/experiments/counter.c @@ -1,8 +1,10 @@ int counter() { + /* A */ int i = 0; - while (i < 100) { + while (/* B */i < 100) { i = i + 1; } + /* C */ return i; } diff --git a/tex/thesis/implementation/experiments/example-output b/tex/thesis/implementation/experiments/example-output index 5194e12..38ce67a 100644 --- a/tex/thesis/implementation/experiments/example-output +++ b/tex/thesis/implementation/experiments/example-output @@ -39,8 +39,8 @@ Succs (1): B3 [B5] - 1: 1 - 2: int x1 = 1; + 1: 0 + 2: int x1 = 0; 3: 1 4: int x2 = 1; Preds (1): B6 @@ -52,104 +52,56 @@ 0-6-pre = max(-inf, inf) 1-6-pre = max(-inf, inf) 2-6-pre = max(-inf, inf) -3-6-pre = max(-inf, inf) -4-6-pre = max(-inf, inf) -5-6-pre = max(-inf, inf) 0-5-pre = max(-inf, 0-6-pre) 1-5-pre = max(-inf, 1-6-pre) 2-5-pre = max(-inf, 2-6-pre) -3-5-pre = max(-inf, 3-6-pre) -4-5-pre = max(-inf, 4-6-pre) -5-5-pre = max(-inf, 5-6-pre) -0-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -1-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -2-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) -3-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -4-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -5-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) +0-5-0 = max(-inf, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)) +1-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))) +2-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))) 0-2-pre = max(-inf, 0-5-0, 0-3-pre) 1-2-pre = max(-inf, 1-5-0, 1-3-pre) 2-2-pre = max(-inf, 2-5-0, 2-3-pre) -3-2-pre = max(-inf, 3-5-0, 3-3-pre) -4-2-pre = max(-inf, 4-5-0, 4-3-pre) -5-2-pre = max(-inf, 5-5-0, 5-3-pre) 0-4-pre = max(-inf, min(8, 0-2-pre)) 1-4-pre = max(-inf, 1-2-pre) 2-4-pre = max(-inf, 2-2-pre) -3-4-pre = max(-inf, 3-2-pre) -4-4-pre = max(-inf, 4-2-pre) -5-4-pre = max(-inf, 5-2-pre) 0-1-pre = max(-inf, 0-2-pre) -1-1-pre = max(-inf, min(-9, 1-2-pre)) +1-1-pre = max(-inf, 1-2-pre) 2-1-pre = max(-inf, 2-2-pre) -3-1-pre = max(-inf, 3-2-pre) -4-1-pre = max(-inf, 4-2-pre) -5-1-pre = max(-inf, 5-2-pre) -0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -1-4-0 = max(-inf, add(-2, MCF<[1,-1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -2-4-0 = max(-inf, MCF<[0,1,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) -3-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -4-4-0 = max(-inf, add(-2, MCF<[1,0,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -5-4-0 = max(-inf, MCF<[0,-1,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))) +1-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))) +2-4-0 = max(-inf, MCF<[0,-1,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre)) 0-3-pre = max(-inf, 0-4-0) 1-3-pre = max(-inf, 1-4-0) 2-3-pre = max(-inf, 2-4-0) -3-3-pre = max(-inf, 3-4-0) -4-3-pre = max(-inf, 4-4-0) -5-3-pre = max(-inf, 5-4-0) 0-0-pre = max(-inf, 0-1-pre) 1-0-pre = max(-inf, 1-1-pre) 2-0-pre = max(-inf, 2-1-pre) -3-0-pre = max(-inf, 3-1-pre) -4-0-pre = max(-inf, 4-1-pre) -5-0-pre = max(-inf, 5-1-pre) Block 0: x1 <= 10 - -x1 <= -9 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 1: x1 <= 10 - -x1 <= -9 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 2: x1 <= 10 - -x1 <= -1 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 3: x1 <= 10 - -x1 <= -3 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -3 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 4: x1 <= 8 - -x1 <= -1 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 5: x1 <= inf - -x1 <= inf - x1 - x2 <= inf x2 <= inf - -x2 <= inf - x2 - x1 <= inf + x2-x1 <= inf Block 6: x1 <= inf - -x1 <= inf - x1 - x2 <= inf x2 <= inf - -x2 <= inf - x2 - x1 <= inf + x2-x1 <= inf diff --git a/tex/thesis/implementation/experiments/example.c b/tex/thesis/implementation/experiments/example.c index 39b65f2..0010804 100644 --- a/tex/thesis/implementation/experiments/example.c +++ b/tex/thesis/implementation/experiments/example.c @@ -1,11 +1,13 @@ int example() { + /* A */ int x1 = 1; int x2 = 1; - while (x1 <= 8) { + while (/* B */ x1 <= 8) { x1 = x1 + 2; x2 = x2 + 2; } + /* C */ return x2; } diff --git a/tex/thesis/implementation/experiments/fib-output b/tex/thesis/implementation/experiments/fib-output index 900f636..ec86733 100644 --- a/tex/thesis/implementation/experiments/fib-output +++ b/tex/thesis/implementation/experiments/fib-output @@ -65,345 +65,107 @@ 3-6-pre = max(-inf, inf) 4-6-pre = max(-inf, inf) 5-6-pre = max(-inf, inf) -6-6-pre = max(-inf, inf) -7-6-pre = max(-inf, inf) -8-6-pre = max(-inf, inf) -9-6-pre = max(-inf, inf) -10-6-pre = max(-inf, inf) -11-6-pre = max(-inf, inf) -12-6-pre = max(-inf, inf) -13-6-pre = max(-inf, inf) -14-6-pre = max(-inf, inf) -15-6-pre = max(-inf, inf) -16-6-pre = max(-inf, inf) -17-6-pre = max(-inf, inf) -18-6-pre = max(-inf, inf) -19-6-pre = max(-inf, inf) 0-5-pre = max(-inf, 0-6-pre) 1-5-pre = max(-inf, 1-6-pre) 2-5-pre = max(-inf, 2-6-pre) 3-5-pre = max(-inf, 3-6-pre) 4-5-pre = max(-inf, 4-6-pre) 5-5-pre = max(-inf, 5-6-pre) -6-5-pre = max(-inf, 6-6-pre) -7-5-pre = max(-inf, 7-6-pre) -8-5-pre = max(-inf, 8-6-pre) -9-5-pre = max(-inf, 9-6-pre) -10-5-pre = max(-inf, 10-6-pre) -11-5-pre = max(-inf, 11-6-pre) -12-5-pre = max(-inf, 12-6-pre) -13-5-pre = max(-inf, 13-6-pre) -14-5-pre = max(-inf, 14-6-pre) -15-5-pre = max(-inf, 15-6-pre) -16-5-pre = max(-inf, 16-6-pre) -17-5-pre = max(-inf, 17-6-pre) -18-5-pre = max(-inf, 18-6-pre) -19-5-pre = max(-inf, 19-6-pre) -0-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -1-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -2-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -3-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -4-5-0 = max(-inf, add(1, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -5-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -6-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -7-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -8-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -9-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -10-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -11-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -12-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -13-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -14-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -15-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -16-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -17-5-0 = max(-inf, add(-1, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) -18-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) -19-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) +0-5-0 = max(-inf, add(1, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) +1-5-0 = max(-inf, add(-1, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) +2-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) +3-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) +4-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) +5-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) 0-2-pre = max(-inf, 0-5-0, 0-3-pre) 1-2-pre = max(-inf, 1-5-0, 1-3-pre) 2-2-pre = max(-inf, 2-5-0, 2-3-pre) 3-2-pre = max(-inf, 3-5-0, 3-3-pre) 4-2-pre = max(-inf, 4-5-0, 4-3-pre) 5-2-pre = max(-inf, 5-5-0, 5-3-pre) -6-2-pre = max(-inf, 6-5-0, 6-3-pre) -7-2-pre = max(-inf, 7-5-0, 7-3-pre) -8-2-pre = max(-inf, 8-5-0, 8-3-pre) -9-2-pre = max(-inf, 9-5-0, 9-3-pre) -10-2-pre = max(-inf, 10-5-0, 10-3-pre) -11-2-pre = max(-inf, 11-5-0, 11-3-pre) -12-2-pre = max(-inf, 12-5-0, 12-3-pre) -13-2-pre = max(-inf, 13-5-0, 13-3-pre) -14-2-pre = max(-inf, 14-5-0, 14-3-pre) -15-2-pre = max(-inf, 15-5-0, 15-3-pre) -16-2-pre = max(-inf, 16-5-0, 16-3-pre) -17-2-pre = max(-inf, 17-5-0, 17-3-pre) -18-2-pre = max(-inf, 18-5-0, 18-3-pre) -19-2-pre = max(-inf, 19-5-0, 19-3-pre) 0-4-pre = max(-inf, 0-2-pre) 1-4-pre = max(-inf, 1-2-pre) 2-4-pre = max(-inf, 2-2-pre) 3-4-pre = max(-inf, 3-2-pre) -4-4-pre = max(-inf, 4-2-pre) +4-4-pre = max(-inf, min(19, 4-2-pre)) 5-4-pre = max(-inf, 5-2-pre) -6-4-pre = max(-inf, 6-2-pre) -7-4-pre = max(-inf, 7-2-pre) -8-4-pre = max(-inf, 8-2-pre) -9-4-pre = max(-inf, 9-2-pre) -10-4-pre = max(-inf, min(19, 10-2-pre)) -11-4-pre = max(-inf, 11-2-pre) -12-4-pre = max(-inf, 12-2-pre) -13-4-pre = max(-inf, 13-2-pre) -14-4-pre = max(-inf, 14-2-pre) -15-4-pre = max(-inf, 15-2-pre) -16-4-pre = max(-inf, 16-2-pre) -17-4-pre = max(-inf, 17-2-pre) -18-4-pre = max(-inf, 18-2-pre) -19-4-pre = max(-inf, 19-2-pre) 0-1-pre = max(-inf, 0-2-pre) 1-1-pre = max(-inf, 1-2-pre) 2-1-pre = max(-inf, 2-2-pre) 3-1-pre = max(-inf, 3-2-pre) 4-1-pre = max(-inf, 4-2-pre) -5-1-pre = max(-inf, 5-2-pre) -6-1-pre = max(-inf, 6-2-pre) -7-1-pre = max(-inf, 7-2-pre) -8-1-pre = max(-inf, 8-2-pre) -9-1-pre = max(-inf, 9-2-pre) -10-1-pre = max(-inf, 10-2-pre) -11-1-pre = max(-inf, min(-20, 11-2-pre)) -12-1-pre = max(-inf, 12-2-pre) -13-1-pre = max(-inf, 13-2-pre) -14-1-pre = max(-inf, 14-2-pre) -15-1-pre = max(-inf, 15-2-pre) -16-1-pre = max(-inf, 16-2-pre) -17-1-pre = max(-inf, 17-2-pre) -18-1-pre = max(-inf, 18-2-pre) -19-1-pre = max(-inf, 19-2-pre) -0-4-0 = max(-inf, MCF<[-2,1,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -1-4-0 = max(-inf, MCF<[2,-1,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -2-4-0 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -3-4-0 = max(-inf, MCF<[-1,1,1,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -4-4-0 = max(-inf, MCF<[-1,0,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -5-4-0 = max(-inf, MCF<[-1,0,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -6-4-0 = max(-inf, MCF<[1,0,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -7-4-0 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -8-4-0 = max(-inf, MCF<[0,0,1,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -9-4-0 = max(-inf, MCF<[0,-1,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -10-4-0 = max(-inf, MCF<[-1,0,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -11-4-0 = max(-inf, MCF<[1,0,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -12-4-0 = max(-inf, MCF<[1,-1,-1,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -13-4-0 = max(-inf, MCF<[0,0,-1,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -14-4-0 = max(-inf, MCF<[0,-1,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -15-4-0 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -16-4-0 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -17-4-0 = max(-inf, MCF<[1,0,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -18-4-0 = max(-inf, MCF<[0,1,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -19-4-0 = max(-inf, MCF<[0,1,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) -0-4-1 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -1-4-1 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -2-4-1 = max(-inf, MCF<[0,1,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -3-4-1 = max(-inf, add(-1, MCF<[0,1,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -4-4-1 = max(-inf, MCF<[0,1,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -5-4-1 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -6-4-1 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -7-4-1 = max(-inf, MCF<[0,-1,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -8-4-1 = max(-inf, add(-1, MCF<[0,0,0,-1,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -9-4-1 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -10-4-1 = max(-inf, add(1, MCF<[-1,0,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -11-4-1 = max(-inf, add(-1, MCF<[1,0,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -12-4-1 = max(-inf, add(1, MCF<[0,-1,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -13-4-1 = max(-inf, add(1, MCF<[0,0,0,1,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -14-4-1 = max(-inf, add(1, MCF<[0,0,0,1,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) -15-4-1 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -16-4-1 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -17-4-1 = max(-inf, MCF<[0,-1,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -18-4-1 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) -19-4-1 = max(-inf, add(-1, MCF<[0,0,0,-1,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) +5-1-pre = max(-inf, min(-20, 5-2-pre)) +0-4-0 = max(-inf, MCF<[-2,1,1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +1-4-0 = max(-inf, MCF<[2,-1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +2-4-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +3-4-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +4-4-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +5-4-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +0-4-1 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0)) +1-4-1 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0)) +2-4-1 = max(-inf, MCF<[-1,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0)) +3-4-1 = max(-inf, MCF<[1,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0)) +4-4-1 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0))) +5-4-1 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0))) 0-3-pre = max(-inf, 0-4-1) 1-3-pre = max(-inf, 1-4-1) 2-3-pre = max(-inf, 2-4-1) 3-3-pre = max(-inf, 3-4-1) 4-3-pre = max(-inf, 4-4-1) 5-3-pre = max(-inf, 5-4-1) -6-3-pre = max(-inf, 6-4-1) -7-3-pre = max(-inf, 7-4-1) -8-3-pre = max(-inf, 8-4-1) -9-3-pre = max(-inf, 9-4-1) -10-3-pre = max(-inf, 10-4-1) -11-3-pre = max(-inf, 11-4-1) -12-3-pre = max(-inf, 12-4-1) -13-3-pre = max(-inf, 13-4-1) -14-3-pre = max(-inf, 14-4-1) -15-3-pre = max(-inf, 15-4-1) -16-3-pre = max(-inf, 16-4-1) -17-3-pre = max(-inf, 17-4-1) -18-3-pre = max(-inf, 18-4-1) -19-3-pre = max(-inf, 19-4-1) 0-0-pre = max(-inf, 0-1-pre) 1-0-pre = max(-inf, 1-1-pre) 2-0-pre = max(-inf, 2-1-pre) 3-0-pre = max(-inf, 3-1-pre) 4-0-pre = max(-inf, 4-1-pre) 5-0-pre = max(-inf, 5-1-pre) -6-0-pre = max(-inf, 6-1-pre) -7-0-pre = max(-inf, 7-1-pre) -8-0-pre = max(-inf, 8-1-pre) -9-0-pre = max(-inf, 9-1-pre) -10-0-pre = max(-inf, 10-1-pre) -11-0-pre = max(-inf, 11-1-pre) -12-0-pre = max(-inf, 12-1-pre) -13-0-pre = max(-inf, 13-1-pre) -14-0-pre = max(-inf, 14-1-pre) -15-0-pre = max(-inf, 15-1-pre) -16-0-pre = max(-inf, 16-1-pre) -17-0-pre = max(-inf, 17-1-pre) -18-0-pre = max(-inf, 18-1-pre) -19-0-pre = max(-inf, 19-1-pre) Block 0: fib <= 1 -fib <= -1 - fib - fib_last <= 1 - fib - i <= 1 - fib - temp_fib <= inf - fib_last <= 1 - -fib_last <= 0 - fib_last - fib <= 0 - fib_last - i <= 0 - fib_last - temp_fib <= inf + fib_last <= inf + -fib_last <= inf i <= 20 -i <= -20 - i - fib <= 19 - i - fib_last <= 19 - i - temp_fib <= inf - temp_fib <= inf - -temp_fib <= inf - temp_fib - fib <= inf - temp_fib - fib_last <= inf - temp_fib - i <= inf Block 1: fib <= 1 -fib <= -1 - fib - fib_last <= 1 - fib - i <= 1 - fib - temp_fib <= inf - fib_last <= 1 - -fib_last <= 0 - fib_last - fib <= 0 - fib_last - i <= 0 - fib_last - temp_fib <= inf + fib_last <= inf + -fib_last <= inf i <= 20 -i <= -20 - i - fib <= 19 - i - fib_last <= 19 - i - temp_fib <= inf - temp_fib <= inf - -temp_fib <= inf - temp_fib - fib <= inf - temp_fib - fib_last <= inf - temp_fib - i <= inf Block 2: - fib <= 39 - -fib <= -1 - fib - fib_last <= 19 - fib - i <= 37 - fib - temp_fib <= inf - fib_last <= 38 - -fib_last <= 0 - fib_last - fib <= 0 - fib_last - i <= inf - fib_last - temp_fib <= inf + fib <= inf + -fib <= inf + fib_last <= inf + -fib_last <= inf i <= 20 -i <= 0 - i - fib <= 19 - i - fib_last <= 19 - i - temp_fib <= inf - temp_fib <= inf - -temp_fib <= inf - temp_fib - fib <= inf - temp_fib - fib_last <= inf - temp_fib - i <= inf Block 3: fib <= inf - -fib <= -1 - fib - fib_last <= inf - fib - i <= inf - fib - temp_fib <= inf + -fib <= inf fib_last <= inf - -fib_last <= -1 - fib_last - fib <= 0 - fib_last - i <= inf - fib_last - temp_fib <= 0 + -fib_last <= inf i <= 20 -i <= -1 - i - fib <= 19 - i - fib_last <= 19 - i - temp_fib <= 19 - temp_fib <= inf - -temp_fib <= -1 - temp_fib - fib <= 0 - temp_fib - fib_last <= 0 - temp_fib - i <= inf Block 4: fib <= inf - -fib <= -1 - fib - fib_last <= inf - fib - i <= inf - fib - temp_fib <= inf + -fib <= inf fib_last <= inf - -fib_last <= 0 - fib_last - fib <= 0 - fib_last - i <= inf - fib_last - temp_fib <= inf + -fib_last <= inf i <= 19 -i <= 0 - i - fib <= 19 - i - fib_last <= 19 - i - temp_fib <= inf - temp_fib <= inf - -temp_fib <= inf - temp_fib - fib <= inf - temp_fib - fib_last <= inf - temp_fib - i <= inf Block 5: fib <= inf -fib <= inf - fib - fib_last <= inf - fib - i <= inf - fib - temp_fib <= inf fib_last <= inf -fib_last <= inf - fib_last - fib <= inf - fib_last - i <= inf - fib_last - temp_fib <= inf i <= inf -i <= inf - i - fib <= inf - i - fib_last <= inf - i - temp_fib <= inf - temp_fib <= inf - -temp_fib <= inf - temp_fib - fib <= inf - temp_fib - fib_last <= inf - temp_fib - i <= inf Block 6: fib <= inf -fib <= inf - fib - fib_last <= inf - fib - i <= inf - fib - temp_fib <= inf fib_last <= inf -fib_last <= inf - fib_last - fib <= inf - fib_last - i <= inf - fib_last - temp_fib <= inf i <= inf -i <= inf - i - fib <= inf - i - fib_last <= inf - i - temp_fib <= inf - temp_fib <= inf - -temp_fib <= inf - temp_fib - fib <= inf - temp_fib - fib_last <= inf - temp_fib - i <= inf diff --git a/tex/thesis/implementation/experiments/nested-output b/tex/thesis/implementation/experiments/nested-output index d6b55be..15e95c2 100644 --- a/tex/thesis/implementation/experiments/nested-output +++ b/tex/thesis/implementation/experiments/nested-output @@ -82,10 +82,6 @@ 5-9-pre = max(-inf, inf) 6-9-pre = max(-inf, inf) 7-9-pre = max(-inf, inf) -8-9-pre = max(-inf, inf) -9-9-pre = max(-inf, inf) -10-9-pre = max(-inf, inf) -11-9-pre = max(-inf, inf) 0-8-pre = max(-inf, 0-9-pre) 1-8-pre = max(-inf, 1-9-pre) 2-8-pre = max(-inf, 2-9-pre) @@ -94,22 +90,14 @@ 5-8-pre = max(-inf, 5-9-pre) 6-8-pre = max(-inf, 6-9-pre) 7-8-pre = max(-inf, 7-9-pre) -8-8-pre = max(-inf, 8-9-pre) -9-8-pre = max(-inf, 9-9-pre) -10-8-pre = max(-inf, 10-9-pre) -11-8-pre = max(-inf, 11-9-pre) -0-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -1-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -2-8-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -3-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -4-8-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -5-8-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -6-8-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -7-8-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -8-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -9-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -10-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) -11-8-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre)) +0-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +1-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +2-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +3-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +4-8-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +5-8-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +6-8-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) +7-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre)) 0-2-pre = max(-inf, 0-8-0, 0-3-0) 1-2-pre = max(-inf, 1-8-0, 1-3-0) 2-2-pre = max(-inf, 2-8-0, 2-3-0) @@ -118,46 +106,30 @@ 5-2-pre = max(-inf, 5-8-0, 5-3-0) 6-2-pre = max(-inf, 6-8-0, 6-3-0) 7-2-pre = max(-inf, 7-8-0, 7-3-0) -8-2-pre = max(-inf, 8-8-0, 8-3-0) -9-2-pre = max(-inf, 9-8-0, 9-3-0) -10-2-pre = max(-inf, 10-8-0, 10-3-0) -11-2-pre = max(-inf, 11-8-0, 11-3-0) -0-7-pre = max(-inf, min(9, 0-2-pre)) +0-7-pre = max(-inf, 0-2-pre) 1-7-pre = max(-inf, 1-2-pre) -2-7-pre = max(-inf, 2-2-pre) +2-7-pre = max(-inf, min(9, 2-2-pre)) 3-7-pre = max(-inf, 3-2-pre) 4-7-pre = max(-inf, 4-2-pre) 5-7-pre = max(-inf, 5-2-pre) 6-7-pre = max(-inf, 6-2-pre) 7-7-pre = max(-inf, 7-2-pre) -8-7-pre = max(-inf, 8-2-pre) -9-7-pre = max(-inf, 9-2-pre) -10-7-pre = max(-inf, 10-2-pre) -11-7-pre = max(-inf, 11-2-pre) 0-1-pre = max(-inf, 0-2-pre) -1-1-pre = max(-inf, min(-10, 1-2-pre)) +1-1-pre = max(-inf, 1-2-pre) 2-1-pre = max(-inf, 2-2-pre) -3-1-pre = max(-inf, 3-2-pre) +3-1-pre = max(-inf, min(-10, 3-2-pre)) 4-1-pre = max(-inf, 4-2-pre) 5-1-pre = max(-inf, 5-2-pre) 6-1-pre = max(-inf, 6-2-pre) 7-1-pre = max(-inf, 7-2-pre) -8-1-pre = max(-inf, 8-2-pre) -9-1-pre = max(-inf, 9-2-pre) -10-1-pre = max(-inf, 10-2-pre) -11-1-pre = max(-inf, 11-2-pre) -0-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -1-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -2-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -3-7-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -4-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -5-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -6-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -7-7-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -8-7-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -9-7-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -10-7-0 = max(-inf, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) -11-7-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)) +0-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +1-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +2-7-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +3-7-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +4-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +5-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +6-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) +7-7-0 = max(-inf, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre)) 0-4-pre = max(-inf, 0-7-0, 0-5-0) 1-4-pre = max(-inf, 1-7-0, 1-5-0) 2-4-pre = max(-inf, 2-7-0, 2-5-0) @@ -166,10 +138,6 @@ 5-4-pre = max(-inf, 5-7-0, 5-5-0) 6-4-pre = max(-inf, 6-7-0, 6-5-0) 7-4-pre = max(-inf, 7-7-0, 7-5-0) -8-4-pre = max(-inf, 8-7-0, 8-5-0) -9-4-pre = max(-inf, 9-7-0, 9-5-0) -10-4-pre = max(-inf, 10-7-0, 10-5-0) -11-4-pre = max(-inf, 11-7-0, 11-5-0) 0-0-pre = max(-inf, 0-1-pre) 1-0-pre = max(-inf, 1-1-pre) 2-0-pre = max(-inf, 2-1-pre) @@ -178,10 +146,6 @@ 5-0-pre = max(-inf, 5-1-pre) 6-0-pre = max(-inf, 6-1-pre) 7-0-pre = max(-inf, 7-1-pre) -8-0-pre = max(-inf, 8-1-pre) -9-0-pre = max(-inf, 9-1-pre) -10-0-pre = max(-inf, 10-1-pre) -11-0-pre = max(-inf, 11-1-pre) 0-6-pre = max(-inf, 0-4-pre) 1-6-pre = max(-inf, 1-4-pre) 2-6-pre = max(-inf, 2-4-pre) @@ -190,10 +154,6 @@ 5-6-pre = max(-inf, 5-4-pre) 6-6-pre = max(-inf, 6-4-pre) 7-6-pre = max(-inf, 7-4-pre) -8-6-pre = max(-inf, 8-4-pre) -9-6-pre = max(-inf, 9-4-pre) -10-6-pre = max(-inf, 10-4-pre) -11-6-pre = max(-inf, 11-4-pre) 0-3-pre = max(-inf, 0-4-pre) 1-3-pre = max(-inf, 1-4-pre) 2-3-pre = max(-inf, 2-4-pre) @@ -202,22 +162,14 @@ 5-3-pre = max(-inf, min(-10, 5-4-pre)) 6-3-pre = max(-inf, 6-4-pre) 7-3-pre = max(-inf, 7-4-pre) -8-3-pre = max(-inf, 8-4-pre) -9-3-pre = max(-inf, 9-4-pre) -10-3-pre = max(-inf, 10-4-pre) -11-3-pre = max(-inf, 11-4-pre) -0-6-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)) -1-6-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)) -2-6-0 = max(-inf, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)) -3-6-0 = max(-inf, add(-1, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))) -4-6-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)) -5-6-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)) -6-6-0 = max(-inf, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)) -7-6-0 = max(-inf, add(-1, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))) -8-6-0 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))) -9-6-0 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))) -10-6-0 = max(-inf, add(1, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))) -11-6-0 = max(-inf, add(1, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))) +0-6-0 = max(-inf, add(1, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))) +1-6-0 = max(-inf, add(-1, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))) +2-6-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)) +3-6-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)) +4-6-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)) +5-6-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)) +6-6-0 = max(-inf, add(1, MCF<[0,1,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))) +7-6-0 = max(-inf, add(1, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))) 0-5-pre = max(-inf, 0-6-0) 1-5-pre = max(-inf, 1-6-0) 2-5-pre = max(-inf, 2-6-0) @@ -226,162 +178,110 @@ 5-5-pre = max(-inf, 5-6-0) 6-5-pre = max(-inf, 6-6-0) 7-5-pre = max(-inf, 7-6-0) -8-5-pre = max(-inf, 8-6-0) -9-5-pre = max(-inf, 9-6-0) -10-5-pre = max(-inf, 10-6-0) -11-5-pre = max(-inf, 11-6-0) -0-3-0 = max(-inf, add(1, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))) -1-3-0 = max(-inf, add(-1, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))) -2-3-0 = max(-inf, add(1, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))) -3-3-0 = max(-inf, add(1, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))) -4-3-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)) -5-3-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)) -6-3-0 = max(-inf, add(-1, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))) -7-3-0 = max(-inf, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)) -8-3-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)) -9-3-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)) -10-3-0 = max(-inf, add(-1, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))) -11-3-0 = max(-inf, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)) -0-5-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)) -1-5-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)) -2-5-0 = max(-inf, add(-1, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))) -3-5-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)) -4-5-0 = max(-inf, add(1, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))) -5-5-0 = max(-inf, add(-1, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))) -6-5-0 = max(-inf, add(1, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))) -7-5-0 = max(-inf, add(1, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))) -8-5-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)) -9-5-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)) -10-5-0 = max(-inf, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)) -11-5-0 = max(-inf, add(-1, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))) +0-3-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)) +1-3-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)) +2-3-0 = max(-inf, add(1, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))) +3-3-0 = max(-inf, add(-1, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))) +4-3-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)) +5-3-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)) +6-3-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)) +7-3-0 = max(-inf, add(-1, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))) +0-5-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)) +1-5-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)) +2-5-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)) +3-5-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)) +4-5-0 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))) +5-5-0 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))) +6-5-0 = max(-inf, add(-1, MCF<[0,1,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))) +7-5-0 = max(-inf, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)) Block 0: + result <= 0 + -result <= 0 i <= 0 -i <= -10 - i - j <= inf - i - result <= 0 j <= inf -j <= inf - j - i <= inf - j - result <= inf + result-j <= inf + result-i <= 0 +Block 1: result <= 0 -result <= 0 - result - i <= 0 - result - j <= inf -Block 1: i <= 0 -i <= -10 - i - j <= inf - i - result <= 0 j <= inf -j <= inf - j - i <= inf - j - result <= inf + result-j <= inf + result-i <= 0 +Block 2: result <= 0 -result <= 0 - result - i <= 0 - result - j <= inf -Block 2: i <= 0 -i <= 0 - i - j <= inf - i - result <= 0 j <= inf -j <= inf - j - i <= inf - j - result <= inf - result <= 0 - -result <= 0 - result - i <= 0 - result - j <= inf + result-j <= inf + result-i <= 0 Block 3: + result <= 10 + -result <= 0 i <= 0 -i <= 0 - i - j <= 0 - i - result <= 0 j <= 10 -j <= -10 - j - i <= 10 - j - result <= 0 + result-j <= 0 + result-i <= 10 +Block 4: result <= 10 -result <= 0 - result - i <= 10 - result - j <= 0 -Block 4: i <= 0 -i <= 0 - i - j <= 0 - i - result <= 0 j <= 10 -j <= 0 - j - i <= 10 - j - result <= 0 - result <= 10 - -result <= 0 - result - i <= 10 - result - j <= 0 + result-j <= 0 + result-i <= 10 Block 5: + result <= 10 + -result <= -1 i <= 0 -i <= 0 - i - j <= 0 - i - result <= -1 j <= 9 -j <= 0 - j - i <= 9 - j - result <= -1 - result <= 10 - -result <= -1 - result - i <= 10 - result - j <= 1 + result-j <= 1 + result-i <= 10 Block 6: + result <= 10 + -result <= 0 i <= 0 -i <= 0 - i - j <= 0 - i - result <= 0 j <= 9 -j <= 0 - j - i <= 10 - j - result <= 0 - result <= 10 - -result <= 0 - result - i <= 10 - result - j <= 0 + result-j <= 0 + result-i <= 10 Block 7: + result <= 0 + -result <= 0 i <= 0 -i <= 0 - i - j <= inf - i - result <= 0 j <= inf -j <= inf - j - i <= inf - j - result <= inf - result <= 0 - -result <= 0 - result - i <= 0 - result - j <= inf + result-j <= inf + result-i <= 0 Block 8: + result <= inf + -result <= inf i <= inf -i <= inf - i - j <= inf - i - result <= inf j <= inf -j <= inf - j - i <= inf - j - result <= inf + result-j <= inf + result-i <= inf +Block 9: result <= inf -result <= inf - result - i <= inf - result - j <= inf -Block 9: i <= inf -i <= inf - i - j <= inf - i - result <= inf j <= inf -j <= inf - j - i <= inf - j - result <= inf - result <= inf - -result <= inf - result - i <= inf - result - j <= inf + result-j <= inf + result-i <= inf |