Commit 79e07b5f authored by Dan Frumin's avatar Dan Frumin

FLOCK FREE ADMIT THREE

parent cd9c189a
...@@ -423,9 +423,7 @@ Section flock. ...@@ -423,9 +423,7 @@ Section flock.
iFrame. iSplitR ; [ | iSplitL "Haprops"]. iFrame. iSplitR ; [ | iSplitL "Haprops"].
- iPureIntro. - iPureIntro.
rewrite /from_active map_fmap_singleton /=. rewrite /from_active map_fmap_singleton /=.
(* TODO: RK, please look at this *) apply map_disjoint_singleton_r, lookup_delete.
admit.
- rewrite /from_active map_fmap_singleton /=. - rewrite /from_active map_fmap_singleton /=.
rewrite -insert_union_singleton_r. rewrite -insert_union_singleton_r.
2: { apply lookup_delete. } 2: { apply lookup_delete. }
...@@ -448,7 +446,7 @@ Section flock. ...@@ -448,7 +446,7 @@ Section flock.
iMod ("Hcl" with "[-]") as "_". iMod ("Hcl" with "[-]") as "_".
{ iNext. iLeft. iFrame. } { iNext. iLeft. iFrame. }
iModIntro. iPureIntro. rewrite map_fmap_singleton //. iModIntro. iPureIntro. rewrite map_fmap_singleton //.
Admitted. Qed.
Lemma release_cancel_spec γ lk i X : Lemma release_cancel_spec γ lk i X :
{{{ is_flock γ lk flocked γ {[i:=X]} }}} {{{ is_flock γ lk flocked γ {[i:=X]} }}}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment