Ahhh! Lots of things.

6 files changed, 474 insertions, 541 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
diff --git a/tex/thesis/implementation/implementation.tex b/tex/thesis/implementation/implementation.tex
index 02f2180..287cf8d 100644
--- a/tex/thesis/implementation/implementation.tex
+++ b/tex/thesis/implementation/implementation.tex
@@ -21,22 +21,198 @@ presented in Chapter \ref{chap:contribution}. The primary difference
 is the use of objects instead of higher-order functions, as C++'s
 support for higher-order functions was insufficient for our purposes.
 
-The solver was developed using only the STL for the core of the
-solver. A front-end was developed using the ANTLR parser generator
-\cite{antlr} to test the solver separately to the LLVM/Clang
-integration.
+The solver was developed using only the Standard Template
+Library~\cite{stl} for the core of the solver. A front-end was
+developed using the ANTLR parser generator \cite{antlr} to test the
+solver without the equation system generation of the clang framework.
 
+A high level overview of the implementation is presented in Figure
+\ref{fig:solver-arch}. The strategy iteration and fixpoint iteration
+loops provide feedback to each other about which values have changed
+at each iteration, continuing until the strategy stabilises.
+
+\begin{figure}
+  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+      distance=4cm,main node/.style={rectangle,draw,minimum
+        height=2cm,minimum width=3cm}]
+
+    \node[main node] (maximiser) {Strategy iteration};
+    \node[main node] (minimiser) [below of=maximiser] {Fixpoint iteration};
+    \node (input) [node distance=5cm,left of=maximiser] {\emph{input}};
+    \node (output) [node distance=5cm,right of=minimiser] {\emph{output}};
+
+    \path []
+    (input) edge node {Equation system} (maximiser)
+    (maximiser) edge [bend left] node {Improved strategy} (minimiser)
+    (minimiser) edge [bend left] node [align=center]{Greatest fixpoint \\ of strategy} (maximiser)
+    (minimiser) edge node [align=center] {Least fixpoint \\ of system} (output)
+    ;
+
+  \end{tikzpicture}
+  \caption{A very high level overview of the solver implementation.}
+  \label{fig:solver-arch}
+\end{figure}
+
+In the following subsections we provide some timings for two general
+classes of equation systems. Each of the equation systems consists
+solely of inexpensive operations, either a variable lookup or a
+constant term, so we are comparing only the effect of the algorithms
+without consideration of the expense of calculating subexpressions.
+
+All these measurements were performed on a Core 2 Duo E8400 with 4GB
+of memory running Debian sid. Binaries were compiled with GCC 4.7.2
+with the -O3 flag. The source code for the solver is available
+online~\cite{bitbucket-repo}.
 
 \subsection{Chain}
 
+Our first class of example equation systems is a chain. These equation
+systems have the following form:
+\begin{align*}
+  x_0 &= \max(-inf, 0) \\
+  x_1 &= \max(-inf, x_0) \\
+  ... &~ ... \\
+  x_n &= \max(-inf, x_{n-1})
+\end{align*}
+
+This particular class of equation system is the simplest of the class
+of equations with acyclic dependency graphs. In this particular case
+our solver significantly outperforms the naive algorithm for most
+problem sizes. For equation systems of less than four variables the
+naive approach is slightly faster, but this is of no real practical
+concern as in both cases it takes less than a millisecond to provide a
+result.
+
+\begin{figure}
+  \begin{tikzpicture}
+    \begin{loglogaxis}[% 
+        scale only axis,
+        width=0.7\textwidth,
+        height=10cm,
+        xmin=1, xmax=65536,
+        xlabel=size of equation system,
+        ymin=0, ymax=250,
+        ylabel=time (in seconds),
+        axis on top,
+        legend entries={DSI, Naive}]
 
+      \addplot coordinates{ 
+        (1,0.000018267)
+        (2,0.000042359)
+        (4,0.000077031)
+        (8,0.000155439)
+        (16,0.000308687)
+        (32,0.000570927)
+        (64,0.001190886)
+        (128,0.002441834)
+        (256,0.004609652)
+        (512,0.009588408)
+        (1024,0.018226228)
+        (2048,0.036292838)
+        (4096,0.076125736)
+        (8192,0.152150204)
+        (16384,0.307867610)
+        (32768,0.654639048)
+        (65536,1.190741627)
+      };
+
+      \addplot coordinates{ 
+        (1,0.000012504 )
+        (2,0.000021558 )
+        (4,0.000060316 )
+        (8,0.000276887 )
+        (16,0.001414449 )
+        (32,0.009278044 )
+        (64,0.067620090 )
+        (128,0.508776074 )
+        (256,3.939142736 )
+        (512,31.373059038 )
+        (1024,246.603110160 )
+      };
+
+    \end{loglogaxis}
+  \end{tikzpicture}
+  \caption{Chart comparing the performance of our DSI algorithm
+    compared to a naive approach on simple chain examples. Note that
+    both axes are logarithmic.}
+  \label{fig:solver-chain}
+\end{figure}
 
 
 \subsection{Cycle}
 
+The next class of equation system we will consider will be long
+\emph{cycles}. These will 
+\begin{align*}
+  x_0 &= \max(-inf, 0, x_n) \\
+  x_1 &= \max(-inf, x_0) \\
+  ... &~ ... \\
+  x_n &= \max(-inf, x_{n-1})
+\end{align*}
 
+Our dependency graph is no longer acyclic, so finding the value of any
+one variable requires the evaluation, and potential strategy
+improvement, of all other values. The chart in Figure
+\ref{fig:solver-cycle} shows the running time of the DSI algorithm
+again, showing that the addition of an acyclic dependency does not
+have a significant effect.
+
+
+\begin{figure}
+  \begin{tikzpicture}
+    \begin{loglogaxis}[% 
+        scale only axis,
+        width=0.7\textwidth,
+        height=10cm,
+        xmin=1, xmax=65536,
+        xlabel=size of equation system,
+        ymin=0, ymax=250,
+        ylabel=time (in seconds),
+        axis on top,
+        legend entries={DSI, Naive}]
+
+      \addplot coordinates{ 
+        (1,0.000016665)
+        (2,0.000044187)
+        (4,0.000081627)
+        (8,0.000159545)
+        (16,0.000309742)
+        (32,0.000627197)
+        (64,0.001236493)
+        (128,0.002338711)
+        (256,0.004967883)
+        (512,0.009164379)
+        (1024,0.018700068)
+        (2048,0.041385796)
+        (4096,0.073920841)
+        (8192,0.150712424)
+        (16384,0.302473783)
+        (32768,0.665616132)
+        (65536,1.220667681)
+      };
+
+      \addplot coordinates{ 
+        (1,0.000012877 )
+        (2,0.000021507 )
+        (4,0.000059573 )
+        (8,0.000252723 )
+        (16,0.001419862 )
+        (32,0.009221822 )
+        (64,0.067315559 )
+        (128,0.500673679 )
+        (256,3.912675638 )
+        (512,31.750177791 )
+        (1024,249.912189424 )
+      };
+
+    \end{loglogaxis}
+  \end{tikzpicture}
+  \caption{Chart comparing the performance of our DSI algorithm
+    compared to a naive approach on simple cyclical examples. Note
+    that both axes are logarithmic.}
+  \label{fig:solver-cycle}
+\end{figure}
 
-\subsection{Dense}
 
 
 
@@ -66,11 +242,13 @@ different points in the program.
     \node[main node,fill=red!60] (eqns) [below of=clang-analysis]
          {Zone analysis};
     \node[main node] (dsi) [below of=eqns] {DSI};
-    \node (reality) [node distance=5cm,right of=eqns] {};
+    \node (input) [node distance=7cm,left of=clang-analysis] {\emph{input}};
+    \node (reality) [node distance=5cm,right of=eqns] {\emph{output}};
 
     \path []
     %(clang) edge[bend right] node[anchor=east] {CFG} (clang-analysis)
-    (clang-analysis) edge[bend right] node[anchor=east] {CFG} (eqns)
+    (input) edge node {Source code} (clang-analysis)
+    (clang-analysis) edge node[anchor=east] {CFG} (eqns)
     (eqns) edge[bend right] node[anchor=east] {Equation System} (dsi)
     (dsi) edge[bend right] node[anchor=west] {Solution} (eqns)
     (eqns) edge node[anchor=north] {Variable bounds} (reality)
@@ -84,28 +262,165 @@ different points in the program.
 \end{figure}
 
 
-\pagebreak
-\subsection{Chain}
-\lstinputlisting{implementation/experiments/chain.c}
+In the sections which follow we present the results of evaluating our
+analysis pass on several small programs. The full output from our tool
+is provided in Appendix~\ref{appendix:tool-output}, but a condensed
+form of the equation systems and variable bounds is presented here. In
+the following equation systems we use $MCF\{G\}$ to denote the minimum
+cost flow through the flow network $G$.
 
 \pagebreak
 \subsection{Counter}
 \lstinputlisting{implementation/experiments/counter.c}
 
-\lstinputlisting{implementation/experiments/backwards_counter.c}
+This program is extremely simple, consisting only of incrementing a
+variable repeatedly in a loop. It is possible to gain a precise result
+from a widening and narrowing on this function, so we also achieve a
+precise result with this approach.
 
-\pagebreak
-\subsection{Nested Loops}
-\lstinputlisting{implementation/experiments/nested.c}
+Since we only have a single variable, we only wish to determine the
+bounds on $i$ and $-i$. Thus, we have the following equation system:
+\begin{align*}
+  ub(i)_A &= \infty \\
+  -lb(i)_A &= \infty \\
+  ub(i)_B &= \max(-\infty, 0,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+    distance=2cm]
+    \node (i)[draw,circle] {$1$};
+    \node (dummy)[draw,circle,right of=i] {$-1$};
+    \path [use as bounding box] (0,0) rectangle (0.5,1);
+    \path
+    (i) edge[->,bend left] node {$\min(ub(i)_B, 99)$} (dummy)
+    (dummy) edge[->,bend left] node {$-lb(i)_B$} (i);
+  \end{tikzpicture}\right\} + 1) \\
+%
+  -lb(i)_B &= \max(-\infty, 0,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+    distance=2cm]
+    \node (i)[draw,circle] {$-1$};
+    \node (dummy)[draw,circle,right of=i] {$1$};
+    \path [use as bounding box] (0,0) rectangle (0.5,1);
+    \path
+    (i) edge[->,bend left] node {$\min(ub(i)_B, 99)$} (dummy)
+    (dummy) edge[->,bend left] node {$-lb(i)_B$} (i);
+  \end{tikzpicture}\right\} - 1) \\
+%
+%
+  ub(i)_C &= \max(-\infty,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+    distance=2.5cm]
+    \node (i)[draw,circle] {$1$};
+    \node (dummy)[draw,circle,right of=i] {$-1$};
+    \path [use as bounding box] (0,0) rectangle (0.75,1.25);
+    \path
+    (i) edge[->,bend left] node {$ub(i)_B$} (dummy)
+    (dummy) edge[->,bend left] node {$\min(-lb(i)_B, -100)$} (i);
+  \end{tikzpicture}\right\}) \\
+%
+  -lb(i)_C &= \max(-\infty,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+    distance=2.5cm]
+    \node (i)[draw,circle] {$-1$};
+    \node (dummy)[draw,circle,right of=i] {$1$};
+    \path [use as bounding box] (0,0) rectangle (0.75,1.25);
+    \path
+    (i) edge[->,bend left] node {$ub(i)_B$} (dummy)
+    (dummy) edge[->,bend left] node {$\min(-lb(i)_B, -100)$} (i);
+  \end{tikzpicture}\right\})
+\end{align*}
+
+Solving this system of equations gives us the following bounds on $i$:
+\\
+\begin{center}
+  \begin{tabular}{c|cc}
+    Block & ub(i) & lb(i) \\
+    \hline 
+    A & $\infty$ & $-\infty$ \\
+    B & $100$ & $0$ \\
+    C & $100$ & $-100$
+  \end{tabular}
+\end{center}
+
+This is a precise analysis of the values of $i$, performed without
+widening/narrowing. It captures the possible values of $i$ precisely
+and identifies the value of $i$ at the exit of the loop.
 
 \pagebreak
 \subsection{Double counting}
 \lstinputlisting{implementation/experiments/example.c}
 
-\pagebreak
-\subsection{Fibonacci}
-\lstinputlisting{implementation/experiments/fib.c}
+In this example we are incrementing two different program variables at
+the same time, based on a condition of one of the variables. In
+standard interval analysis it is impossible to capture the
+relationship between these variables, but by performing abstract
+interpretation over zones we can perform a more precise analysis.
 
-\pagebreak
-\subsection{Unreachable}
-\lstinputlisting{implementation/experiments/irreducible.c}
+This example is a translation to C of the example presented by
+Gawlitza et al.~\cite{EasyChair:117}. In our abstract analysis we will
+consider the values $x1$, $x2$ and $x2 - x1$.
+
+\begin{align*}
+  ub(x1)_A &= \infty \\
+  ub(x2)_A &= \infty \\
+  ub(x2 - x1)_A &= \infty \\
+%
+  ub(x1)_B &= \max(-\infty, 0,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+        distance=2.5cm]
+      \node (x1)[draw,circle] {$1$};
+      \node (x2)[draw,circle,below of=x1] {$0$};
+      \node (dummy)[draw,circle,below right of=x1] {$-1$};
+      \path
+      (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
+      (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
+      (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
+    \end{tikzpicture}\right\} + 2) \\
+  ub(x2)_B &= \max(-\infty, 1,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+        distance=2.5cm]
+      \node (x1)[draw,circle] {$0$};
+      \node (x2)[draw,circle,below of=x1] {$1$};
+      \node (dummy)[draw,circle,below right of=x1] {$-1$};
+      \path
+      (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
+      (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
+      (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
+    \end{tikzpicture}\right\} + 2) \\
+  ub(x2 - x1)_B &= \max(-\infty, 1,
+  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+        distance=2.5cm]
+      \node (x1)[draw,circle] {$-1$};
+      \node (x2)[draw,circle,below of=x1] {$1$};
+      \node (dummy)[draw,circle,below right of=x1] {$0$};
+      \path
+      (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
+      (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
+      (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
+    \end{tikzpicture}\right\})  \\
+%
+%
+  ub(x1)_C &= \max(-\infty, ub(x1)_B)  \\
+  ub(x2)_C &= \max(-\infty, ub(x2)_B)  \\
+  ub(x2 - x1)_C &= \max(-\infty, ub(x2 - x1)_B)
+\end{align*}
+
+
+Solving this system of equations gives us the following bounds on
+$x1,x2$ and $x2-x1$:
+\\
+\begin{center}
+  \begin{tabular}{c|ccc}
+    Block & ub(x1) & ub(x2) & ub(x2 - x1) \\
+    \hline 
+    A & $\infty$ & $\infty$ & $\infty$ \\
+    B & $10$ & $11$ & $1$ \\
+    C & $10$ & $11$ & $1$
+  \end{tabular} 
+\end{center}
+
+This result is more precise than any that could have been obtained by
+interval analysis. We accurately capture the relationship between $x1$
+and $x2$ by bounding $x2 - x1 \le 1$, and this allows us to correctly
+determine the upper bound of $x2$ at the exit of the loop. The output
+of our automatic analysis for this function can be seen in Section
+\ref{sec:example-function-output}.