enrich
   persistence-state
, 
   nat-list-set
, 
   group-store, 
   index-store, 
   error-class
, 
   eraseblock
, 
   address-data

with
   

   
   
   functions  elems . : nat-list → nat-set;
              crash-logblock : group-block × nat → group-block;
              crash : index-store × index-store → index-store;
              crash : group-store × group-store × nat-set × nat-list → group-store;
   predicates  inv : nat-list × group-store × group-store × nat-set × index-store × index-store;
               inv-journal : nat-list × group-store × group-store × nat-set;
               inv-index : index-store × index-store;
               inv-state : persistence-state × nat-list × group-store × index-store × bool;
   
   variables  ginval : nat-set;
              maxino : nat;
              syn : bool;
   
   

   

   axioms crash-index-in :  ⊦ n ∈ crash(istore, istore0) ↔ n ∈ istore0;
          used for: s, ls;
          crash-index-at :  ⊦ n ∈ istore0 → crash(istore, istore0)[n] = indexblock(istore[n].indlist, istore[n].ladrlist, istore0[n].ref-size);
          crash-logblock :  ⊦ crash-logblock(gblock, n) = groupblock(gblock.gndlist, gblock.ladrlist, n);
          used for: ls;
          crash-group-in :  ⊦ n ∈ crash(gstore, gstore0, ginval, nx) ↔ n ∈ gstore ∨ n ∈ ginval;
          used for: s, ls;
          crash-group-at
          : ⊦   n ∈ crash(gstore, gstore0, ginval, nx)
              →   crash(gstore, gstore0, ginval, nx)[n]
                = (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gstore[n].gndlist, gstore[n].ladrlist, (n ∈ gstore0 ⊃ gstore0[n].ref-size;0));gstore0[n]);
          used for: s, ls;
          elems-def :  ⊦ n ∈ elems nx ↔ n ∈ nx;
          used for: s, ls;
          inv :  ⊦ inv(nx, gstore, gstore0, ginval, istore, istore0) ↔ ¬ ¬(inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0));
          used for: s, ls;
          inv-journal
          : ⊦   inv-journal(nx, gstore, gstore0, ginval)
              ↔   inv(gstore \ ginval) ∧ inv(gstore0) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval
                ∧ remove-refsize0(gstore0) = gstore0;
          used for: s, ls;
          inv-index :  ⊦ inv-index(istore, istore0) ↔ inv(istore) ∧ inv(istore0) ∧ istore0 ⊑ istore ∧ remove-refsize0(istore0) = istore0;
          used for: s, ls;
          inv-state
          : ⊦   inv-state(pstate, nx, gstore, istore, syn)
              ↔   (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore)
                ∧ (pstate = unbuffered → syn);
          used for: s, ls;

   

   
end enrich