enrich
   FOW, 
   forall-indexWhere
, 
   set-union
with
   functions 
       . | . : List(FOW) × T → List(FOW) prio 8 left;
       . |W : List(FOW) → List(FOW);
       . |FO : List(FOW) → List(FOW);
       . ⊕ . : V × List(FOW) → V;
       . ⊕ . : (L → V) × (L → List(FOW)) → L → V;
   
   predicates 
       ctrok : (L → Nat) × (L → Set(T));
       pendingOk : (L → List(FOW));
       writersOk : (L → List(FOW)) × (L → Set(T));
       notMember : T × (L → Set(T));
       oneMember : T × L × (L → Set(T));
       noPending : T × (L → List(FOW));
       noPendingW : T × (L → List(FOW));
       onePendingW : T × L × (L → List(FOW));
       relyws : T × (L → Set(T)) × (L → Set(T));
       relyws : T × Set(T) × Set(T);
       relyp : T × List(FOW) × List(FOW);
       relyp : T × (L → List(FOW)) × (L → List(FOW));
       FOFollowsW : T × List(FOW);
   
   variables 
       ctr : L → Nat;
       p : L → List(FOW);
       l : L;
       fowl : List(FOW);
       fow : FOW;
       t : T;
       ts : Set(T);
       tsf : L → Set(T);
       writers : L → Set(T);
       readers : L → Set(T);
       n : Nat;
       m : Nat;
       v : V;
       mem : L → V;
   
   
   axioms 
      overwrite-def: ((mem ⊕ p))(l) = mem(l) ⊕ p(l);
      used for: ls;
      
      overwrite-base: v ⊕ [] = v;
      used for: s, ls;
      
      overwrite-rec1: v ⊕ (FO(t) ' + fowl) = v ⊕ fowl;
      used for: s, ls;
      
      overwrite-rec2: v ⊕ (W(v0, t) ' + fowl) = v0 ⊕ fowl;
      used for: s, ls;
      
      FOFollowsW-def: 
      FOFollowsW(t, fowl) ↔ (∀ n. n < # fowl ∧ fowl[n].W? ∧ fowl[n].tid = t → (∃ n0. n < n0 ∧ n0 < # fowl ∧ fowl[n0] = FO(t)));
      
      allrelyws-def: relyws(t, tsf, tsf0) ↔ (∀ l. relyws(t, tsf(l), tsf0(l)));
      
      relyws-def: relyws(t, ts, ts0) ↔ t ∈ ts ↔ t ∈ ts0;
      
      allrelyp-def: relyp(t, p, p0) ↔ (∀ l. relyp(t, p(l), p0(l)));
      
      relyp-def: relyp(t, fowl, fowl0) ↔ (∃ fowl1, fowl2. fowl ⊒ fowl1 ∧ fowl0 = fowl1 + fowl2 ∧ fowl2 | t = []);
      
      filtertid-def: fowl | t = fowl.filter(λ fow. fow.tid = t);
      
      filterwrites-def: fowl |W = fowl.filter(λ fow. fow.W?);
      
      filterfos-def: fowl |FO = fowl.filter(λ fow. fow.FO?);
      
      ctrok-def: ctrok(ctr, writers) ↔ (∀ l. # writers(l) = ctr(l));
      used for: ls;
      
      pendingOk: pendingOk(p) ↔ (∀ l, t. #(p(l) |W | t) ≤ 1);
      used for: ls;
      
      writersOk: writersOk(p, writers) ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []));
      used for: ls;
      
      noWriter: notMember(t, tsf) ↔ (∀ l. ¬ t ∈ tsf(l));
      used for: ls;
      
      oneWriter: oneMember(t, l, tsf) ↔ (∀ l0. t ∈ tsf(l0) ↔ l0 = l);
      used for: ls;
      
      noPending: noPending(t, p) ↔ (∀ l. p(l) | t = []);
      used for: ls;
      
      noPendingW: noPendingW(t, p) ↔ (∀ l. p(l) |W | t = []);
      used for: ls;
      
      onePendingW: onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = []);
      used for: ls;
      comment: at most at one location l pending writes, together with pendingOk we have at most one write pending at l as well;
   
   
end enrich