Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsGlobal.

Set Implicit Arguments.

Ltac kill_upd_irr :=
  intros; match goal with
            | |- ?l _ = ?l _ ⇒ unfold l
            | |- ?l _ _ = ?l _ _ ⇒ unfold l
            | |- ?l _ _ _ = ?l _ _ _ ⇒ unfold l
            | |- ?l _ _ _ _ = ?l _ _ _ _ ⇒ unfold l
            | |- ?l _ _ _ _ _ = ?l _ _ _ _ _ ⇒ unfold l
            | |- ?l _ _ _ _ _ _ = ?l _ _ _ _ _ _ ⇒ unfold l
          end;
  rewrite !map_upd_irr, ?updo; ins; intro;
  repeat (rewrite ?in_map_iff, ?in_flatten_iff in *; desf);
  match goal with H : _ |- _ ⇒ by edestruct H; eauto end.

Lemma in_sb_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Tsb b a) →
    in_sb acts (upd L te r) a = in_sb acts L a.

Lemma in_rf_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Trf b a) →
    in_rf acts (upd L te r) a = in_rf acts L a.

Lemma in_esc_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Tesc b a) →
    in_esc acts (upd L te r) a = in_esc acts L a.

Lemma out_sb_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Tsb a b) → te ≠ TsbS a →
    out_sb acts (upd L te r) a = out_sb acts L a.

Lemma out_rf_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Trf a b) → te ≠ TrfS a →
    out_rf acts (upd L te r) a = out_rf acts L a.

Lemma out_esc_upd_irr :
  ∀ acts L te r EE a,
    (∀ b, te ≠ Tesc a b) →
    (∀ σ, te ≠ TescS σ a) →
    out_esc acts (upd L te r) EE a = out_esc acts L EE a.

Lemma incoming_upd_irr :
  ∀ acts L te r a,
    te_tgt te ≠ Some a →
    incoming acts (upd L te r) a = incoming acts L a.

Lemma outgoing_upd_irr :
  ∀ acts L te r EE a,
    te_src te ≠ a →
    outgoing acts (upd L te r) EE a = outgoing acts L EE a.

Ltac kill_upd_in r :=
  intros; match goal with
            | |- ?l _ = _ ⇒ unfold l
            | |- ?l _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ _ _ _ = _ ⇒ unfold l
          end; match goal with H: In _ _ |- _ ⇒
            apply In_NoDup_Permutation in H; desf;
            rewrite ?(Permutation_rsum (Permutation_map _ (Permutation_map _ H)));
            simpl; rupd; rewrite res_plus_emp_l;
            rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf)
          end; rewrite (res_plusC r); try done; rewrite ?res_plusA; try done.

Lemma in_sb_upd_in :
  ∀ acts L r a b (IN: In a acts) (ND: NoDup acts),
    in_sb acts (upd L (Tsb a b) r) b =
    in_sb acts (upd L (Tsb a b) res_emp) b ⊕ r.

Lemma out_sb_upd_in :
  ∀ acts L r a b (IN: In b acts) (ND: NoDup acts),
    out_sb acts (upd L (Tsb a b) r) a =
    out_sb acts (upd L (Tsb a b) res_emp) a ⊕ r.

Lemma in_rf_upd_in :
  ∀ acts L r a b (IN: In a acts) (ND: NoDup acts),
    in_rf acts (upd L (Trf a b) r) b =
    in_rf acts (upd L (Trf a b) res_emp) b ⊕ r.

Lemma out_rf_upd_in :
  ∀ acts L r a b (IN: In b acts) (ND: NoDup acts),
    out_rf acts (upd L (Trf a b) r) a =
    out_rf acts (upd L (Trf a b) res_emp) a ⊕ r.

Lemma in_esc_upd_in :
  ∀ acts L r a b (IN: In a acts) (ND: NoDup acts),
    in_esc acts (upd L (Tesc a b) r) b =
    in_esc acts (upd L (Tesc a b) res_emp) b ⊕ r.

Lemma out_esc_upd_in1 :
  ∀ acts L EE r a b (IN: In b acts) (ND: NoDup acts),
    out_esc acts (upd L (Tesc a b) r) EE a =
    out_esc acts (upd L (Tesc a b) res_emp) EE a ⊕ r.

Lemma out_esc_upd_in2 :
  ∀ acts L EE r σ a (IN: In σ EE) (ND: NoDup EE),
    out_esc acts (upd L (TescS σ a) r) EE a =
    out_esc acts (upd L (TescS σ a) res_emp) EE a ⊕ r.

Lemma incoming_upd_in :
  ∀ acts L r te b (TGT: te_tgt te = Some b) (IN: In (te_src te) acts) (ND: NoDup acts),
    incoming acts (upd L te r) b =
    incoming acts (upd L te res_emp) b ⊕ r.

Lemma outgoing_upd_in_alt :
  ∀ acts L te b r EE,
    (∀ σ, te = TescS σ b → In σ EE ∧ NoDup EE) →
    (∀ a, te_tgt te = Some a → In a acts ∧ NoDup acts) →
    te_src te = b →
    outgoing acts (upd L te r) EE b =
    outgoing acts (upd L te res_emp) EE b ⊕ r.

Lemma outgoing_upd_in :
  ∀ acts L te b r1 r EE,
    (∀ σ, te = TescS σ b → In σ EE ∧ NoDup EE) →
    (∀ a, te_tgt te = Some a → In a acts ∧ NoDup acts) →
    te_src te = b →
    L te = r1 →
    outgoing acts (upd L te (r1 ⊕ r)) EE b =
    outgoing acts L EE b ⊕ r.

Lemma outgoing_upd2_acc :
  ∀ acts L te1 r1 r te2 r2 EE b,
    (∀ σ a, te1 = TescS σ a ∨ te2 = TescS σ a → In σ EE ∧ NoDup EE) →
    (∀ a, te_tgt te1 = Some a ∨ te_tgt te2 = Some a → In a acts ∧ NoDup acts) →
    te_src te1 = te_src te2 →
    te1 ≠ te2 →
    L te1 = r1 →
    outgoing acts (upd (upd L te1 (r1 ⊕ r)) te2 r2) EE b =
    outgoing acts (upd L te2 (r2 ⊕ r)) EE b.

Lemma outgoing_upd2_swap :
  ∀ acts L te1 r1 te2 r2 EE b,
    (∀ σ a, te1 = TescS σ a ∨ te2 = TescS σ a → In σ EE ∧ NoDup EE) →
    (∀ a, te_tgt te1 = Some a ∨ te_tgt te2 = Some a → In a acts ∧ NoDup acts) →
    te_src te1 = te_src te2 →
    te1 ≠ te2 →
    outgoing acts (upd (upd L te1 (r1 ⊕ L te2)) te2 r2) EE b =
    outgoing acts (upd L te1 (r1 ⊕ r2)) EE b.

Lemma in_rf_upds acts L a b r :
  NoDup acts →
  In a acts →
  in_rf acts L b = res_emp →
  in_rf acts (upd L (Trf a b) r) b = r.

Lemma replace_out_rf :
  ∀ a b c L acts
    (NEQ: c ≠ b)
    (ND: NoDup acts)
    (EMP: L (Trf a b) = res_emp),
  out_rf acts (upd L (Trf a b) (res_strip (out_rf acts L a))) c = out_rf acts L c.

Lemma replace_out_rf2 :
  ∀ a b acts c L
    (ND: NoDup acts)
    (INa: In a acts)
    (INb: In b acts)
    (EQ: L (TrfS a) = out_rf acts L a),
    out_rf (acts)
           (upd (upd L (TrfS a) (res_strip (out_rf acts L a)))
           (Trf a b) (out_rf acts L a)) c =
    out_rf acts L c.

Lemma replace_edge_emp :
  ∀ A (a : A) f pi l
    (EMP: f a = res_emp)
    (ND: NoDup l)
    (IN : In a l),
  rsum (map (upd f a pi) l) = pi ⊕ rsum (map f l).

Lemma helper2 A f (x : A) l :
  NoDup l →
  res_strip (f x) ⊕ rsum (map f l) = Rundef →
  rsum (map f (undup (x :: l))) = Rundef.

Lemma replace_out_sb :
  ∀ a b c L r1 r2 acts (ND: NoDup acts) (IN : In b acts)
    (EMP: L (Tsb a b) ⊕ L (TsbS a) = r1 ⊕ r2),
  out_sb acts (upd (upd L (Tsb a b) r1) (TsbS a) r2) c = out_sb acts L c.

Lemma out_esc_upd_in :
  ∀ acts L σ b r1 r EE,
    In σ EE →
    NoDup EE →
    L (TescS σ b) = r1 →
    out_esc acts (upd L (TescS σ b) (r1 ⊕ r)) EE b =
    out_esc acts L EE b ⊕ r.

Lemma replace_outgoing :
  ∀ te1 te2 b
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (S : te_tgt te2 = Some b)
    acts (ND: NoDup acts) (IN' : In b acts)
    EE (NDE: NoDup EE)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    L r1 r2 (EQ: L te1 ⊕ L te2 = r1 ⊕ r2) c,
  outgoing acts (upd (upd L te1 r1) te2 r2) EE c =
  outgoing acts L EE c.

Lemma safe_mon IE n e QQ r m : safe IE n e QQ r → m ≤ n → safe IE m e QQ r.

Lemma helper_plus_insb_rfS_def :
  ∀ a b acts amap sb rf mo sc L E
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (CC: compat amap sb rf L)
    (IN: In a acts)
    (NIN: ¬ In b acts)
    (LR : label_restr (b::acts) amap sb rf L E),
  in_sb (b :: acts) L b ⊕ L (TrfS a) ≠ Rundef.

Lemma helper_plus_inc_escS_def :
  ∀ a b acts amap sb rf mo sc L E σ
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (CC: compat amap sb rf L)
    (IN: In a acts)
    (NIN: ¬ In b acts)
    (LR : label_restr (b::acts) amap sb rf L E),
  incoming (b :: acts) L b ⊕ L (TescS σ a) ≠ Rundef.

Lemma helper_plus_inc_sbS_back_def :
  ∀ a b acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts)
    (CC: compat amap sb rf L)
    (MO: mo b a)
    (LR : label_restr acts amap sb rf L E),
  incoming acts L a ⊕ L (TsbS b) ≠ Rundef.

Lemma compat_upd1 :
  ∀ amap sb rf L
    (CC : compat amap sb rf L) te r
    (LT : res_lt r (L te)),
  compat amap sb rf (upd L te r).

Lemma compat_upd2 :
  ∀ amap sb rf L
    (CC : compat amap sb rf L) te1 te2
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (NEQ : te1 ≠ te2) r1
    (LT1 : res_lt r1 (L te1)) r2
    (LT2 : res_lt (r1 ⊕ r2) (L te1 ⊕ L te2)),
  compat amap sb rf (upd (upd L te1 r1) te2 r2).

Lemma compat_upd2_bot :
  ∀ amap sb rf L
    (CC : compat amap sb rf L) te1 te2
    (T1 : te_tgt te1 = None)
    (T2 : te_tgt te2 = None)
    (HB : happens_before amap sb rf (te_src te1) (te_src te2))
    (NEQ : te1 ≠ te2) r1
    (LT1 : res_lt r1 (L te1)) r2
    (LT2 : res_lt (r1 ⊕ r2) (L te1 ⊕ L te2)),
  compat amap sb rf (upd (upd L te1 r1) te2 r2).

Lemma compat_upd2_acc :
  ∀ amap sb rf L te1 r1 r
    (CC : compat amap sb rf (upd L te1 (r1 ⊕ r))) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2) r2
    (L2 : r2 = L te2 ⊕ r),
  compat amap sb rf (upd (upd L te1 r1) te2 r2).

Lemma compat_upd2_swap :
  ∀ amap sb rf L te1 r1 r2
    (CC : compat amap sb rf (upd L te1 (r1 ⊕ r2))) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2),
  compat amap sb rf (upd (upd L te1 (r1 ⊕ L te2)) te2 r2).

Lemma compat_upd3 :
  ∀ amap sb rf L te3 rr
    (CC : compat amap sb rf (upd L te3 rr)) te1 te2
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (TS : te_tgt te2 = Some (te_src te3))
    (T' : te_tgt te3 = None)
    (HB : happens_before amap sb rf (te_src te1) (te_src te3))
    (NEQ : te1 ≠ te2)
    (NEQ' : te1 ≠ te3) r1
    (LT1 : res_lt r1 (L te1)) r2 r3
    (LT2 : res_lt (r1 ⊕ r2) (L te1 ⊕ L te2))
    (LT3 : res_lt (r1 ⊕ r3) (L te1 ⊕ rr)),
  compat amap sb rf (upd (upd (upd L te1 r1) te2 r2) te3 r3).

Lemma compat_guar1 amap sb rf L σ b r :
  compat amap sb rf (upd L (TescS σ b) (L (TescS σ b) ⊕ r)) →
  compat amap sb rf (upd L (TsbS b) r).

Lemma compat_guar2 amap sb rf L te r l pi :
  (res_get r l = p_uninit ∨ ∃ v, res_get r l = p_na pe_full v) →
  compat amap sb rf (upd L te r) →
  compat amap sb rf (upd L te (res_upd r l pi)).

Lemma compat_mon_upd amap sb rf L a r :
  compat amap sb rf (upd L a (L a ⊕ r)) →
  compat amap sb rf L.

Lemma conform_upd_irr :
  ∀ acts amap mo L acts',
    conform acts amap mo L acts' →
    ∀ b r,
      conform acts amap mo (upd L (TsbS b) r) acts'.

Lemma conform_ext_irr :
  ∀ acts amap sb rf mo sc L acts',
    Consistent acts amap sb rf mo sc →
    conform acts amap mo L acts' →
    ∀ b,
      (∀ l, ¬ is_writeL (amap b) l) →
      conform acts amap mo L (b::acts').

Lemma valid_node_upd_irr :
  ∀ IE acts amap rf L E te a r
    (S: a ≠ te_src te)
    (T: te_tgt te ≠ Some a)
    (V: valid_node IE acts acts amap rf L E a),
  valid_node IE acts acts amap rf (upd L te r) E a.

Lemma valid_node_upd_esc :
  ∀ IE acts amap rf L EE a
    (V : valid_node IE acts acts amap rf L EE a)
    σ (INs : In σ EE) (ND': NoDup EE)
    b (INb: In b acts) (ND: NoDup acts) (NEQ : a ≠ b),
  valid_node IE acts acts amap rf
     (upd (upd L (TescS σ a) res_emp) (Tesc a b)
        (L (TescS σ a) ⊕ L (Tesc a b))) EE a.

Lemma valid_node_ext_helper :
  ∀ IE acts N amap rf L E a
    (V : valid_node IE acts N amap rf L E a) b,
    is_rmw (amap b) = false →
    valid_node IE acts (b :: N) amap rf L E a.

Lemma valid_node_ext_helper2 :
  ∀ IE acts N amap rf L E a
    (V : valid_node IE acts N amap rf L E a) b,
    rf b ≠ Some a →
    valid_node IE acts (b :: N) amap rf L E a.

Lemma exch_conform_irr1 IE acts amap sb rf L L' EE σ
  (ECO : exch_conform IE acts amap sb rf L L' EE σ) te b
  (TGT: te_tgt te = Some b) r :
  exch_conform IE acts amap sb rf (upd L te r) L' EE σ.

Lemma exch_conform_dec_irr1 IE acts amap sb rf L L' EE σ
  (ECO : exch_conform IE acts amap sb rf L L' EE σ) te
  (NEQ: ∀ a, te ≠ TescS σ a) r
  (LT: res_lt r (L te))
  (DEF: L te ≠ Rundef) :
  exch_conform IE acts amap sb rf (upd L te r) L' EE σ.

Lemma exch_conform_upd2_acc :
  ∀ IE acts amap sb rf L L' EE σ te1 r1 r
    (EX : exch_conform IE acts amap sb rf L (upd L' te1 (r1 ⊕ r)) EE σ) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2) r2
    (L2 : r2 = L' te2 ⊕ r)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    (IN2: ∀ σ, te2 = TescS σ (te_src te1) → In σ EE)
    (NDE: NoDup EE),
  exch_conform IE acts amap sb rf L (upd (upd L' te2 r2) te1 r1) EE σ.

Lemma exch_conform_upd2_swap :
  ∀ IE acts amap sb rf L L' EE σ te1 r1 r2
    (EX : exch_conform IE acts amap sb rf L (upd L' te1 (r1 ⊕ r2)) EE σ) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    (IN2: ∀ σ, te2 = TescS σ (te_src te1) → In σ EE)
    (NDE: NoDup EE),
  exch_conform IE acts amap sb rf L (upd (upd L' te1 (r1 ⊕ L' te2)) te2 r2) EE σ.

Lemma exch_conform_upd3 :
  ∀ IE acts amap sb rf L L' EE σ te3 rr
    (EX : exch_conform IE acts amap sb rf L (upd L' te3 rr) EE σ) te1 te2
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (TS : te_tgt te2 = Some (te_src te3))
    (T' : te_tgt te3 = None)
    (NEQ : te1 ≠ te2)
    (NEQ' : te1 ≠ te3)
    (NEQ'': te_src te1 ≠ te_src te3) r2 r4
    (EQ'' : r2 = L' te2 ⊕ r4) r1
    (EQ : r1 ⊕ L' te2 ⊕ r4 = L' te1 ⊕ L' te2) r3
    (EQ' : r3 = rr ⊕ r4)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    (IN2: ∀ σ, te3 = TescS σ (te_src te3) → In σ EE)
    (INM: In (te_src te2) acts)
    (INN: In (te_src te3) acts)
    (NDA: NoDup acts)
    (NDE: NoDup EE)
    (DEF: outgoing acts (upd L' te3 rr) EE (te_src te3) ⊕ r4 ≠ Rundef)
    (EMP: ∀ gl
       (M1 : res_gget (incoming acts L' (te_src te3)) gl = None)
       (M2 : res_gget (outgoing acts (upd L' te3 rr) EE (te_src te3)) gl ≠ None),
       res_gget r4 gl = None),
  exch_conform IE acts amap sb rf L (upd (upd (upd L' te1 r1) te2 r2) te3 r3) EE σ.

Lemma exch_conform_helper1 :
  ∀ IE acts amap sb rf L L' EE (ND: NoDup EE) σ r r' a
         (ECO: exch_conform IE acts amap sb rf L (upd L' (TsbS a) r) EE σ)
         (IMP: ∀ gl (GNA: res_gget r' gl = None), res_gget r gl = None)
         (OUT: outgoing acts (upd L' (TsbS a) r') EE a ≠ Rundef),
    exch_conform IE acts amap sb rf L (upd L' (TsbS a) r') EE σ.

Lemma ghostalloc_upd2_acc :
  ∀ acts L EE te1 r1 r
    (GAC : ghost_alloc_conform acts (upd L te1 (r1 ⊕ r)) EE) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2) r2
    (L2 : r2 = L te2 ⊕ r)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    (IN2: ∀ σ, te2 = TescS σ (te_src te1) → In σ EE)
    (NDE: NoDup EE),
  ghost_alloc_conform acts (upd (upd L te2 r2) te1 r1) EE.

Lemma ghostalloc_upd2_swap :
  ∀ acts L EE te1 r1 r2
    (GAC: ghost_alloc_conform acts (upd L te1 (r1 ⊕ r2)) EE) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    (IN2: ∀ σ, te2 = TescS σ (te_src te1) → In σ EE)
    (NDE: NoDup EE),
  ghost_alloc_conform acts (upd (upd L te1 (r1 ⊕ L te2)) te2 r2) EE.

Lemma ghostalloc_upd3 :
  ∀ acts L EE te3 rr
    (CC : ghost_alloc_conform acts (upd L te3 rr) EE) te1 te2
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (TS : te_tgt te2 = Some (te_src te3))
    (T' : te_tgt te3 = None)
    (NEQ : te1 ≠ te2)
    (NEQ' : te1 ≠ te3)
    (NEQ'': te_src te1 ≠ te_src te3) r2 r4
    (EQ'' : r2 = L te2 ⊕ r4) r1
    (EQ : r1 ⊕ L te2 ⊕ r4 = L te1 ⊕ L te2) r3
    (EQ' : r3 = rr ⊕ r4)
    (IN1: ∀ σ, te1 = TescS σ (te_src te1) → In σ EE)
    (IN2: ∀ σ, te3 = TescS σ (te_src te3) → In σ EE)
    (INM: In (te_src te2) acts)
    (INN: In (te_src te3) acts)
    (NDA: NoDup acts)
    (NDE: NoDup EE)
    (DEF: outgoing acts (upd L te3 rr) EE (te_src te3) ⊕ r4 ≠ Rundef),
  ghost_alloc_conform acts (upd (upd (upd L te1 r1) te2 r2) te3 r3) EE.

Lemma ghost_alloc_helper1 :
  ∀ acts L EE (ND: NoDup EE) b r r' a gl,
    ghost_alloc (outgoing acts (upd L (TsbS b) r) EE a) gl →
    outgoing acts (upd L (TsbS b) r) EE b ≠ Rundef →
    (ghost_alloc r gl → ghost_alloc r' gl) →
    ghost_alloc (outgoing acts (upd L (TsbS b) r') EE a) gl.

Lemma ghost_alloc_conform_helper1 :
  ∀ acts L EE (ND: NoDup EE) r r' a
         (GAC: ghost_alloc_conform acts (upd L (TsbS a) r) EE)
         (IMP: ∀ gl (GA: ghost_alloc r' gl), ghost_alloc r gl)
         (OUT: outgoing acts (upd L (TsbS a) r') EE a ≠ Rundef),
    ghost_alloc_conform acts (upd L (TsbS a) r') EE.