Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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