Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav07_homework_4_solution [2007/06/16 21:58]
vkuncak
sav07_homework_4_solution [2007/06/16 22:12] (current)
vkuncak
Line 51: Line 51:
  
 $X \rightarrow Y$: Let $s.c_2 \subseteq G$.  Let $Q = s.c_2$. ​ Then $s.c_2 \subseteq Q$, so also $s.c_1 \subseteq Q$.  Thus $s.c_1 \subseteq s.c_2$. $X \rightarrow Y$: Let $s.c_2 \subseteq G$.  Let $Q = s.c_2$. ​ Then $s.c_2 \subseteq Q$, so also $s.c_1 \subseteq Q$.  Thus $s.c_1 \subseteq s.c_2$.
 +
  
 ==== Part 5 ==== ==== Part 5 ====
 +
 +**Lemma**: $skip;c \equiv c;skip \equiv c$.
  
 $c_1 \sqsubseteq c_2\ \rightarrow\ c_1;c_3 \sqsubseteq c_2;c_3$: $c_1 \sqsubseteq c_2\ \rightarrow\ c_1;c_3 \sqsubseteq c_2;c_3$:
 
sav07_homework_4_solution.txt · Last modified: 2007/06/16 22:12 by vkuncak
 
© EPFL 2018 - Legal notice