Commit ee8a34f6 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent c73ba9c9
......@@ -193,13 +193,11 @@ Section ex.
iDestruct (ExchangerLocal_graph_snap with "EL") as "#Gs2".
iMod (fupd_mask_subseteq (N)) as "Hclose"; [solve_ndisj|].
iMod (ExchangerInv_ExchangerConsistent with "EI EL") as "[[% _] EI]".
iDestruct (ExchangerInv_graph_master_acc with "[$EI //]") as (q) "[GM Close2]".
iDestruct (graph_master_snap_included with "GM Gs2") as %LeG2%graph_sqsubseteq_E.
iDestruct ("Close2" with "GM") as "GM".
iDestruct (ExchangerInv_graph_snap with "EI Gs2") as %LeG2%graph_sqsubseteq_E.
iMod "Hclose" as "_".
iDestruct "Hown" as (b1' b2') "[Hown >[%Hsize %Eqb1]]".
iMod ("Close" with "[Hown GM]") as "_".
iMod ("Close" with "[Hown EI]") as "_".
{ iNext. iExists G2'. iFrame. iExists b1', b2'. by iFrame. }
iIntros "!>". iApply "Post". iPureIntro.
......
......@@ -94,8 +94,7 @@ Proof.
(* get the right mask to access the exchanger's internal invariant. *)
iApply fupd_wp. iMod (fupd_mask_subseteq (N)); [solve_ndisj|].
iMod (ExchangerInv_ExchangerConsistent with "EI EL") as "[[%EGs %EC] EI]".
iDestruct (ExchangerInv_graph_master_acc with "[$EI //]") as (q) "[GM Close2]".
iDestruct (graph_master_snap_included with "GM Gs2") as %LeG2.
iDestruct (ExchangerInv_graph_snap with "EI Gs2") as %LeG2.
exfalso.
(* We learn that xchg1 and xchg2 are new events inserted into G to get G1,
but G1 only has 1 extra event compared to G. So xchg1 = xchg2.
......
Supports Markdown
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