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_normal:
  ∀ 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: HVlabeled (hf l) HLnormal) (ALL: hf l ≠ HVnone),
  << ALLOC: lab (hb_fst edge) = Aalloc l >> ∨
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >> ∧ << SB: ¬ is_rf edge >> ∧
                   (<< SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnormal >> ∨
                    << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∨
                    << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_read (lab (hb_fst edge)) >>).
Lemma step_back_from_nabla:
  ∀ 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: HVlabeled (hf l) HLnabla) (ALL: hf l ≠ HVnone),
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >> ∧
                   (<< SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∨
                    << SB: ¬ is_rf edge >> ∧ << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLtriangle >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnormal >> ∧
                                              << REL: is_release_write (lab (hb_fst edge)) >>).
Lemma step_back_from_triangle:
  ∀ 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: HVlabeled (hf l) HLtriangle) (ALL: hf l ≠ HVnone),
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >> ∧
                    << SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧
                   (<< LAB´: HVlabeled (hf´ l) HLtriangle >> ∨
                    << LAB´: HVlabeled (hf´ l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>).