| # ax2 = # ndx1, # ax3 = # ndx2, gstore[adr].nd = nd, abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓), dom gstore = dom gstore2, fi = fi2[ndx2.keys, ax3], nodes(gstore ↓, jro0) = nodes(gstore2 ↓, jro0), remove-refsize0(gstore0) = gstore0, range fi2 ∩ ax3.toSet = ∅, range fi2 ∩ ax2.toSet = ∅, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore2 ∪ jro0, fi2[ndx2.keys, ax3].inos < jmaxino, jro1 < jmaxino1, p_os < pmaxino, fi2.inos < jmaxino1, fi0.inos < pmaxino, inv(gstore2 \ jro0), inv(gstore0), inv(gstore \ jro0), key-cons(ndx1), key-cons(nd.key, nd), key-cons(ndx2), nodes-cons(ax2, ndx1, gstore, jro0), nodes-cons(ax3 + adr ' + ax2, ndx2 + nd ' + ndx1, gstore2, jro0), refsize-cons(gstore, range fi2[ndx2.keys, ax3]), refsize-cons(gstore2, range fi2), refsize-cons(gstore0, range fi0), ri-inj(fi2), ri-inj(fi0), nd.key ∈ fi2, adr ∈ gstore, jmaxino1 ≤ jmaxino, pmaxino ≤ jmaxino1, pmaxino ≤ jmaxino, ndx2.keys.toSet ⊆ dom fi2, fi2[ndx2.keys, ax3].lebs ⊆ dom gstore2, fi2.lebs ⊆ dom gstore2, fi0.lebs ⊆ dom gstore0, ndx1.keys.toSet ⊆ dom fi2, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ⟪gjournal_index_store#(nd.key, adr, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid; jmaxino, fi, gstore); ax0 := ax2; ndx0 := ndx1⟫ ( (∃ ax, ndx. # ax = # ndx ∧ ax3 + adr ' + ax2 = ax + ax0 ∧ ndx2 + nd ' + ndx1 = ndx + ndx0 ∧ fi = fi2[ndx.keys, ax]) ∧ dom fi = dom fi2 ∧ inv(gstore \ jro0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ jmaxino1 ≤ jmaxino ∧ fi.inos < jmaxino ∧ refsize-cons(gstore, range fi) ∧ ri-inj(fi) ∧ fi.lebs ⊆ dom gstore ∧ dom gstore = dom gstore2 ∧ nodes-cons(ax0, ndx0, gstore, jro0) ∧ nodes(gstore ↓, jro0) = nodes(gstore2 ↓, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓) ∧ (jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ ¬ # ax2 < # ax0), jmaxino1 = 0, pmaxino = 0, dups(nx), dups(ax3 + ax2), dups(ax3), dups(ax2), adr.lnum ∈ jro0, adr ∈ fi2, adr ∈ ax2, adr ∈ ax3 |
# ax3 = # ndx2, # ax2 = # ndx1, gstore[adr].nd = nd, abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓), dom gstore = dom gstore2, fi = fi2[ndx2.keys, ax3], nodes(gstore ↓, jro0) = nodes(gstore2 ↓, jro0), remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, range fi2 ∩ ax2.toSet = ∅, range fi2 ∩ ax3.toSet = ∅, dom gstore0 ∪ elems nx = dom gstore2 ∪ jro0, jmaxino1 ≠ 0, pmaxino ≠ 0, fi0.inos < pmaxino, fi2.inos < jmaxino1, p_os < pmaxino, jro1 < jmaxino1, fi2[ndx2.keys, ax3].inos < jmaxino, inv(gstore \ jro0), inv(gstore0), inv(gstore2 \ jro0), key-cons(ndx2), key-cons(gstore[adr].nd.key, gstore[adr].nd), key-cons(ndx1), nodes-cons(ax3 + adr ' + ax2, ndx2 + gstore[adr].nd ' + ndx1, gstore2, jro0), nodes-cons(ax2, ndx1, gstore, jro0), refsize-cons(gstore0, range fi0), refsize-cons(gstore2, range fi2), refsize-cons(gstore, range fi2[ndx2.keys, ax3]), ri-inj(fi0), ri-inj(fi2), adr ∈ gstore, gstore[adr].nd.key ∈ fi2, pmaxino ≤ jmaxino, pmaxino ≤ jmaxino1, jmaxino1 ≤ jmaxino, ndx1.keys.toSet ⊆ dom fi2, fi0.lebs ⊆ dom gstore0, fi2.lebs ⊆ dom gstore2, fi2[ndx2.keys, ax3].lebs ⊆ dom gstore2, ndx2.keys.toSet ⊆ dom fi2, ¬ dups(ax2), ¬ dups(ax3), ¬ dups(ax3 + ax2), ¬ dups(nx), ¬ adr ∈ ax3, ¬ adr ∈ ax2, ¬ adr ∈ fi2, ¬ adr.lnum ∈ jro0, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ⟪gjournal_index_store#(gstore[adr].nd.key, adr, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid; jmaxino, fi, gstore); ax0 := ax2; ndx0 := ndx1⟫ ( (∃ ax, ndx. # ax = # ndx ∧ ax3 + adr ' + ax2 = ax + ax0 ∧ ndx2 + nd ' + ndx1 = ndx + ndx0 ∧ fi = fi2[ndx.keys, ax]) ∧ dom fi = dom fi2 ∧ inv(gstore \ jro0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ jmaxino1 ≤ jmaxino ∧ fi.inos < jmaxino ∧ refsize-cons(gstore, range fi) ∧ ri-inj(fi) ∧ fi.lebs ⊆ dom gstore ∧ dom gstore = dom gstore2 ∧ nodes-cons(ax0, ndx0, gstore, jro0) ∧ nodes(gstore ↓, jro0) = nodes(gstore2 ↓, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓) ∧ (jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ ¬ # ax2 < # ax0)