Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas.
Require Import fslhmap.
Set Implicit Arguments.
Lemma step_back_from_normalR:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeledR (hf l) HLnormal),
  << STORE: is_writeL (lab (hb_fst edge)) l >> ∨
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << SB: ¬ is_rf edge >> ∧
                   (<< SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnormal >> ∨
                    << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∨
                    << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_read (lab (hb_fst edge)) >>).
Lemma step_back_from_nablaR:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeledR (hf l) HLnabla),
  (<< STORE: is_writeL (lab (hb_fst edge)) l >> ∧
   << REL: is_release_write (lab (hb_fst edge)) >> ∧
   << RF: ¬ is_sb edge >>) ∨
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧
                   (<< SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∨
                    << SB: ¬ is_rf edge >> ∧ << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLtriangle >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnormal >> ∧
                                              << REL: is_release_write (lab (hb_fst edge)) >>).
Lemma step_back_from_triangleR:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeledR (hf l) HLtriangle),
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧
                    << SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧
                   (<< LAB´: HVlabeledR (hf´ l) HLtriangle >> ∨
                    << LAB´: HVlabeledR (hf´ l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>).