From: Mart Lubbers 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}