fix 1b

diff --git a/first.tex b/first.tex
index 0a9cd85..a5f505b 100644 (file)
--- 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}