enrich
   zbranch-array-sorted
, 
   znode-ops, 
   node-index-restrict
, 
   node-index
, 
   node-store
, 
   index-store
, 
   node-status
with
   

   
   
   functions  payload : zbranch-array × nat × nat → node-index;
              key-range : zbranch-array × nat × nat × node-index → node-index;
              keys : zbranch-array × nat × nat → key-set;
   predicates  nsize : nat × node-status;
               compatible : node-index × node-index × zbranch-array × nat × nat;
               compatible : key-set × key-set × zbranch-array × nat × nat;
               unmodified : address × znode × index-address-store;
               look : bool × key × address × node-index;
   
   variables  ld : key-set;
              ld0 : key-set;
              ld1 : key-set;
              key' : key;
              rp : ref;
              rc : ref;
              dirty : bool;
              dirty0 : bool;
              height : nat;
              nused : nat;
              len : nat;
   
   

   

   axioms nsze-ok :  ⊦ nsize(nused, ok) ↔ nused < BRANCH_SIZE;
          used for: s, ls;
          nsze-overfull :  ⊦ nsize(nused, overfull?) ↔ nused ≤ BRANCH_SIZE;
          used for: s, ls;
          nsze-underfull :  ⊦ nsize(nused, underfull?) ↔ nused < BRANCH_SIZE;
          used for: s, ls;
          ri-compatible
          : nused ≠ 0
            ⊦   compatible(ri0, ri1, zbrar, n, nused)
              ↔ sorted(zbrar, 0, nused - 1) → (∀ m. m ≠ n ∧ m < nused → key-range(zbrar, m, nused, ri0) = key-range(zbrar, m, nused, ri1));
          unmodified :  ⊦ unmodified(adr, znd, iast) ↔ ¬ znd.dirty → adr ∈ iast ∧ iast[adr] = save(znd);
          used for: ls;
          range-one :  ⊦ key-range(zbrar, 0, 1, ri) = ri;
          used for: s, ls;
          range-first :  ⊦ nused ≠ 0 ∧ nused < # zbrar → key-range(zbrar, 0, nused + 1, ri) = ri |≤ zbrar[0].key;
          used for: s, ls;
          range-inner
          :  ⊦ n ≠ 0 ∧ n + 1 < nused ∧ nused ≤ # zbrar → key-range(zbrar, n, nused, ri) = (ri |> zbrar[n - 1].key) |≤ zbrar[n].key;
          used for: s, ls;
          range-last :  ⊦ n ≠ 0 ∧ n < # zbrar → key-range(zbrar, n, n + 1, ri) = ri |> zbrar[n - 1].key;
          used for: s, ls;
          payload-base :  ⊦ payload(zbrar, m, 0) = ∅;
          used for: s, ls;
          payload-rec
          : ⊦   m < # zbrar
              →   payload(zbrar, m, nused + 1)
                = (zbrar[m].entry? ⊃ payload(zbrar, m + 1, nused)[zbrar[m].key, zbrar[m].adr];payload(zbrar, m + 1, nused));
          used for: s, ls;
          keys-base :  ⊦ keys(zbrar, m, 0) = ∅;
          used for: s, ls;
          keys-rec :  ⊦ m < # zbrar → keys(zbrar, m, nused + 1) = keys(zbrar, m + 1, nused) ++ zbrar[m].key;
          used for: s, ls;
          look :  ⊦ look(bv, key, adr, ri) ↔ (bv ↔ key ∈ ri) ∧ (bv → adr = ri[key]);
          used for: ls;

   

   
end enrich