formatting change and proof simplifcation due to Accepted state definition change

theories/logatom/rdcss/rdcss.v

@@ -186,11 +186,9 @@ Section rdcss.
   (* After the prophecy said we are going to win the race, we commit and run the AU,
      switching from [pending] to [accepted]. *)
   Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) :=
-    ((∃ vs, proph p_ghost_winner vs) ∗ Q ∗
-     match proph_winner with
-       None => True
-     | Some p => ⌜p = p_ghost_winner⌝
-     end)%I.
+    ((∃ vs, proph p_ghost_winner vs) ∗
+     Q ∗
+     ⌜match proph_winner with None => True | Some p => p = p_ghost_winner end⌝)%I.
 
   (* The same thread then wins the CmpXchg and moves from [accepted] to [done].
      Then, the [γ_t] token guards the transition to take out [Q].
@@ -463,9 +461,7 @@ Section rdcss.
         iModIntro. iMod "Hgc_close" as "_".
         (* close descr inv *)
         iModIntro. iSplitL "Q Hp_ghost Hp Hvs Hs Hln'".
-        { iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
-          iRight. iSplitL "Hp_ghost"; first by iExists _.
-          destruct (proph_extract_winner vs) eqn:Hvts; iFrame. }
+        { iModIntro. iNext. iExists _. iFrame "Hp". eauto 12 with iFrame. }
         (* close outer inv *)
         iModIntro. iSplitR "Token_a HQ Hn●".
         { by eauto 12 with iFrame. }