enrich
   RWevent, 
   forall-indexWhere

with
   functions 
       . | . : List((RWevent, Bool)) × T → List((RWevent, Bool)) prio 8 left;
       . | . : List((RWevent, Bool)) × Bool → List((RWevent, Bool)) prio 8 left;
       . | . : List((RWevent, Bool)) × L → List((RWevent, Bool)) prio 8 left;
       . |W : List((RWevent, Bool)) → List((RWevent, Bool));
       . |R : List((RWevent, Bool)) → List((RWevent, Bool));
       . ⊕ . : (L → V) × List((RWevent, Bool)) → L → V;
       events : List((RWevent, Bool)) → List(RWevent);
       persistDependentReads : L × List((RWevent, Bool)) → List((RWevent, Bool));
       firstVolWrite : L × List((RWevent, Bool)) → Nat;
   
   predicates 
       . .lastPersistedOrElse ( . ) : List((RWevent, Bool)) × L × Bool;
       allReadsOK : List((RWevent, Bool));
       allReadsOKInd : (L → V) × (L → Bool) × List((RWevent, Bool));
       allWritesOK : List((RWevent, Bool));
       allWritesOKInd : (T → Bool) × (L → Bool) × List((RWevent, Bool));
       rely : T × List((RWevent, Bool)) × List((RWevent, Bool));
       . ⊑p . : List((RWevent, Bool)) × List((RWevent, Bool));
   
   variables 
       vpe : (RWevent, Bool);
       t : T;
       b : Bool;
       h : List((RWevent, Bool));
       l : L;
       v : V;
       el : List(RWevent);
       e : RWevent;
       hPred : List((RWevent, Bool)) → Bool;
       persisted : L → Bool;
       pending : T → Bool;
       n : Nat;
       mem : L → V;
   
   
   axioms 
      rely-def: rely(t, h0, h1) ↔ (∃ h2, h3. h1 = h2 + h3 ∧ h0 ⊑p h2 ∧ h3 | t = []);
      used for: ls;
      
      hist-more-persisted-base1: [] ⊑p h ↔ h = [];
      used for: s, ls;
      
      hist-more-persisted-base2: ¬ vpe ' + h ⊑p [];
      used for: s, ls;
      
      hist-more-persisted-rec: vpe0 ' + h0 ⊑p vpe1 ' + h1 ↔ vpe0._1 = vpe1._1 ∧ (vpe0._2 → vpe1._2) ∧ h0 ⊑p h1;
      used for: s, ls;
      
      allReadsOK-def: allReadsOK(h) ↔ allReadsOKInd(∅, λ l. true, h);
      used for: ls;
      
      allReadsOKInd-base: allReadsOKInd(mem, persisted, []);
      used for: s, ls;
      
      allReadsOKInd-recW: allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h);
      used for: s, ls;
      
      allReadsOKInd-recR: allReadsOKInd(mem, persisted, (R(t, l, v), b) ' + h) ↔ v = mem(l) ∧ (b ↔ persisted(l)) ∧ allReadsOKInd(mem, persisted, h);
      used for: s, ls;
      
      allWritesOK-def: allWritesOK(h) ↔ allWritesOKInd(λ t. false, λ l. true, h);
      used for: ls;
      
      allWritesOKInd-base: allWritesOKInd(pending, persisted, []);
      used for: s, ls;
      
      allWritesOKInd-recW: 
        allWritesOKInd(pending, persisted, (W(t, l, v), b) ' + h)
      ↔ ¬ pending(t) ∧ (b → persisted(l)) ∧ allWritesOKInd(pending(t := ¬ b), persisted(l := b), h);
      used for: s, ls;
      
      allWritesOKInd-recR: allWritesOKInd(pending, persisted, (R(t, l, v), b) ' + h) ↔ allWritesOKInd(pending, persisted, h);
      used for: s, ls;
      
      overwrite-base: mem ⊕ [] = mem;
      used for: s, ls;
      
      overwrite-rec-read: mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h;
      used for: s, ls;
      
      overwrite-rec-write: mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h;
      used for: s, ls;
      
      lastPersistedOrElse-base: [].lastPersistedOrElse(l, b) ↔ b;
      used for: s, ls;
      
      lastPersistedOrElse-recR: ((R(t0, l0, v0), b0) ' + h).lastPersistedOrElse(l, b) ↔ h.lastPersistedOrElse(l, b);
      used for: s, ls;
      
      lastPersistedOrElse-recW: ((W(t0, l0, v0), b0) ' + h).lastPersistedOrElse(l, b) ↔ h.lastPersistedOrElse(l, (l = l0 ⊃ b0;b));
      used for: s, ls;
      
      firstVolWrite-def: firstVolWrite(l, h) = h.indexWhere(λ vpe. vpe._1.W? ∧ vpe._1.l = l ∧ ¬ vpe._2);
      
      restrict-thread: h | t = h.filter(λ vpe. vpe._1.t = t);
      used for: ls;
      
      restrict-vp: h | b = h.filter(λ vpe. vpe._2 ↔ b);
      used for: ls;
      
      restrict-events: events(h) = h.map(λ vpe. vpe._1);
      used for: ls;
      
      restrict-loc: h | l = h.filter(λ vpe. vpe._1.l = l);
      used for: ls;
      
      restrict-W: h |W = h.filter(λ vpe. vpe._1.W?);
      used for: ls;
      
      restrict-R: h |R = h.filter(λ vpe. vpe._1.R?);
      used for: ls;
      
      persistDependentReads-base: persistDependentReads(l, []) = [];
      used for: s, ls;
      
      persistDependentReads-nextwrite: persistDependentReads(l, (W(t, l, v), b) ' + h) = (W(t, l, v), b) ' + h;
      used for: s, ls;
      comment: b should be false;
      
      persistDependentReads-read: persistDependentReads(l, (R(t, l, v), b) ' + h) = (R(t, l, v), true) ' + persistDependentReads(l, h);
      used for: s, ls;
      comment: b should be false;
      
      persistDependentReads-otherwrite: l ≠ l0 → persistDependentReads(l, (W(t, l0, v), b) ' + h) = (W(t, l0, v), b) ' + persistDependentReads(l, h);
      used for: s, ls;
      
      persistDependentReads-otherread: l ≠ l0 → persistDependentReads(l, (R(t, l0, v), b) ' + h) = (R(t, l0, v), b) + persistDependentReads(l, h);
      used for: s, ls;
   
   
end enrich