From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 23 Jun 2016 08:00:00 +0000 (+0200)
Subject: fix 1b
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ccebad95ac4e7b266a7a518059e01cc400f27ec0;p=mc1516the.git

fix 1b
---

diff --git a/first.tex b/first.tex
index 0a9cd85..a5f505b 100644
--- a/first.tex
+++ b/first.tex
@@ -17,19 +17,19 @@ Rajeev Alur. Suppose initially we have a zone $(s0, [0\leq x\leq 4, 0\leq y
 in the derivation.}
 
 We define:\\
-$e_0=\langle s_0, a, [], [x:=0] s_1\rangle$ and\\
-$e_1=\langle s_1, a, [], [y:=0] s_2\rangle$\\
+$e_0=\langle s_0, a, \emptyset, [x:=0] s_1\rangle$ and\\
+$e_1=\langle s_1, a, \emptyset, [y:=0] s_2\rangle$\\
 
 And we derive:\\
 \begin{align*}
 	succ(e_1, succ(e_0, [0\leq x\leq 4, 0\leq y])) =&
-		succ(e_1, ((([0\leq x\leq 4, 0\leq y]\wedge [])\Uparrow)\wedge []\wedge [x<1])[x:=0])\\
-	=& succ(e_1, (([0\leq x\leq 4, 0\leq y]\Uparrow)\wedge []\wedge [x<1])[x:=0])\\
-	=& succ(e_1, ([0\leq x<1, 0\leq y])[x:=0])\\
-	=& succ(e_1, [x=1, 0\leq y][x:=0])\\
-	=& ((([x=1, 0\leq y]\wedge [x<1])\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
-	=& (([x=1, 0\leq y]\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
-	=& [x<1, y=0]
+		succ(e_1, ((([0\leq x\leq 4, 0\leq y]\wedge\emptyset)\Uparrow)\wedge\emptyset\wedge [x<1])[x:=0])\\
+	=& succ(e_1, (([0\leq x\leq 4, 0\leq y]\Uparrow)\wedge\emptyset\wedge [x<1])[x:=0])\\
+	=& succ(e_1, [0\leq x<1, 0\leq y][x:=0])\\
+	=& succ(e_1, [x=0, 0\leq y])\\
+	=& ((([x=0, 0\leq y]\wedge [x<1])\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
+	=& (([0\leq x<1, 0\leq y]\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
+	=& [0\leq x<1, y=0]
 \end{align*}
 
 \subsection*{1.c}