| changeset 289 | a5dd2c966cbe |
| parent 288 | 64c9f151acf5 |
| child 290 | 6a6d0bd16035 |
| 288:64c9f151acf5 | 289:a5dd2c966cbe |
|---|---|
768 qed |
768 qed |
769 qed |
769 qed |
770 qed |
770 qed |
771 |
771 |
772 lemma step_depend_v: |
772 lemma step_depend_v: |
773 fixes th::thread |
|
773 assumes vt: |
774 assumes vt: |
774 "vt step (V th cs#s)" |
775 "vt step (V th cs#s)" |
775 shows " |
776 shows " |
776 depend (V th cs # s) = |
777 depend (V th cs # s) = |
777 depend s - {(Cs cs, Th th)} - |
778 depend s - {(Cs cs, Th th)} - |