enrich
   FLITPSC-preds, 
   Bevent
with
   functions 
       . |WL . : List(Bevent) × L → List(Bevent) prio 8 left;
       . |SF . : List(Bevent) × L → List(Bevent) prio 8 left;
       . .FOWs ( . ) : List(Bevent) × T × L → List(FOW);
       . ⊕ . : V × List(Bevent) → V;
       . ⊕ . : (L → V) × List(Bevent) → L → V;
   
   predicates 
       writersOk : (T → List(Bevent)) × (L → List(FOW)) × (L → Set(T));
       pendingOk : (T → List(Bevent)) × (L → List(FOW));
       noPendingW : T × (T → List(Bevent)) × (L → List(FOW));
       noPending : T × (T → List(Bevent)) × (L → List(FOW));
       isPropFO : Nat × L × List(Bevent);
       FOFollowsW : T × List(Bevent) × (L → List(FOW)) × L;
       FOFollowsW : T × List(Bevent) × List(FOW) × L;
       SFTrailing : (T → List(Bevent));
       . ⊒w . : List(Bevent) × List(Bevent);
       . .FOs? : (T → List(Bevent));
       readFOsOk : (T → List(Bevent)) × (L → Set(T));
       rely : T × (L → List(FOW)) × (T → List(Bevent)) × (L → List(FOW)) × (T → List(Bevent));
       rely : T × L × List(FOW) × List(Bevent) × List(FOW) × List(Bevent);
   
   variables 
       be : Bevent;
       bel : List(Bevent);
       bq : T → List(Bevent);
       rfo : T → List(Bevent);
       l : L;
       v : V;
       mem : L → V;
       t : T;
       p : L → List(FOW);
       pq : L → List(FOW);
       writers : L → Set(T);
       m : Nat;
       n : Nat;
       fow : FOW;
       fowl : List(FOW);
   
   
   axioms 
      overwrite-def: ((mem ⊕ bel))(l) = mem(l) ⊕ (bel |WL l);
      used for: ls;
      
      overwrite-base: v ⊕ [] = v;
      used for: s, ls;
      
      overwrite-rec-FO: v ⊕ (FO(l) ' + bel) = v ⊕ bel;
      used for: s, ls;
      
      overwrite-rec-SF: v ⊕ (SF ' + bel) = v ⊕ bel;
      used for: s, ls;
      
      overwrite-rec-W: v ⊕ (W(l, v0) ' + bel) = v0 ⊕ bel;
      used for: s, ls;
      
      isPropFO-def: isPropFO(n, l, bel) ↔ n < # bel ∧ bel[n] = FO(l) ∧ (∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l));
      
      BrestrictL-def: bel |WL l = bel.filter(λ be. be.W? ∧ be.l = l);
      
      B-restrict-SF-l: bel |SF l = bel.filter(λ be. be = SF ∨ be.l = l);
      used for: ls;
      
      B-postfix-weak: bel0 ⊒w bel1 ↔ (∀ l. bel0 |SF l ⊒ bel1 |SF l);
      used for: ls;
      
      SFTrailing: SFTrailing(bq) ↔ (∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast);
      used for: ls;
      
      FOs: rfo.FOs? ↔ (∀ t. rfo(t).forall(.FO?));
      used for: ls;
      
      readFOsOk: readFOsOk(rfo, writers) ↔ rfo.FOs? ∧ (∀ t, l. t ∈ writers(l) → rfo(t) = []);
      used for: ls;
      
      pendingOk: pendingOk(bq, p) ↔ (∀ l, t. #(p(l) |W | t) + #(bq(t) |WL l) ≤ 1);
      used for: ls;
      
      noPending: noPending(t, bq, p) ↔ (∀ l. p(l) | t = [] ∧ bq(t) = []);
      used for: ls;
      
      noPendingW: noPendingW(t, bq, p) ↔ (∀ l. p(l) |W | t = [] ∧ bq(t) |WL l = []);
      used for: ls;
      
      FOFollowsW-old-def: 
        FOFollowsW(t, bel, p, l)
      ↔   (∀ n. 
               n < # p(l) ∧ p(l)[n].W? ∧ p(l)[n].tid = t
             → (∃ n0. n < n0 ∧ n0 < # p(l) ∧ p(l)[n0] = FO(t) ∨ bel ≠ [] ∧ bel.head = FO(l)))
        ∧ (bel ≠ [] → bel = SF ' ∨ bel = FO(l) ' + SF ' ∨ bel.head.W? ∧ bel.head.l = l ∧ bel.tail = FO(l) ' + SF ');
      
      FOFollowsW-def: 
        FOFollowsW(t, bel, fowl, l)
      ↔   (∀ fowl0, fowl1, v. fowl = fowl0 + W(v, t) ' + fowl1 → FO(t) ∈ fowl1 ∨ FO(l) ∈ bel)
        ∧ (∀ bel0, bel1, v. bel = bel0 + W(l, v) ' + bel1 → FO(l) ∈ bel1);
      
      writersOk: 
        writersOk(bq, p, writers)
      ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = [] ∧ bq(t) |WL l = []));
      used for: ls;
      
      FOWs-base: [].FOWs(t, l) = [];
      used for: s, ls;
      
      FOWs-SF: (SF ' + bel).FOWs(t, l) = bel.FOWs(t, l);
      used for: s, ls;
      
      FOWs-FO: (FO(l0) ' + bel).FOWs(t, l) = (l = l0 ⊃ FO(t) ';[]) + bel.FOWs(t, l);
      used for: s, ls;
      
      FOWs-W: (W(l0, v) ' + bel).FOWs(t, l) = (l = l0 ⊃ W(v, t) ';[]) + bel.FOWs(t, l);
      used for: s, ls;
      
      rely-def: rely(t, pq, bq, pq0, bq0) ↔ (∀ l. rely(t, l, pq(l), bq(t), pq0(l), bq0(t)));
      used for: ls;
      
      rely-local-def: rely(t, l, fowl, bel, fowl0, bel0) ↔ (fowl | t) + bel.FOWs(t, l) ⊒ (fowl0 | t) + bel0.FOWs(t, l);
      used for: ls;
   
   
end enrich