| jvalid0 ↔ jvalid2, as = as0, as1 = fi1[datakeys(key, n, fi1)], dom gstore = dom gstore4, fi = fi2, fi0 = fi1 \ datakeys(key, n, fi1), gstore0 = gstore1, gstore2 = gstore3, gstore4 = gstore3, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro = ∅, as ∩ range fi0 = ∅, dom gstore1 ∪ elems nx = dom gstore3 ∪ jro, p_os < pmaxino, fi1.inos < jmaxino, fi2.inos < pmaxino, gstore =○refsize gstore4, inv(gstore3 \ jro), inv(gstore1), inv-journal(nx, gstore, gstore0, jro), refsize-cons(gstore3, range fi1), refsize-cons(gstore1, range fi2), refsize-cons(gstore, range fi0 ∪ as), ri-inj(fi1 \ datakeys(key, n, fi1)), ri-inj(fi1), ri-inj(fi2), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore3, fi2.lebs ⊆ dom gstore1, as.lebs ⊆ dom gstore, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro), jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro) ⊦ ⟪choose n, adr with adr ∈ as in {index_get_gblock_refsize#(adr.lnum, fi0, fi, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; ; n); index_set_gblock_refsize#(adr.lnum, n - adr.size, fi0, fi, jro, gstore0, nx, pmaxino, p_os, jvalid; gstore); as := as -- adr}⟫ ( ( (jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ dom gstore = dom gstore4 ∧ as ∩ range fi0 = ∅ ∧ as.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi0 ∪ as) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ gstore =○refsize gstore4) ∧ # as < # as0), as = ∅, pmaxino = 0, dups(nx) |
jvalid0 ↔ jvalid2, as = as0, as1 = fi1[datakeys(key, n0, fi1)], dom gstore = dom gstore4, fi = fi2, fi0 = fi1 \ datakeys(key, n0, fi1), gstore0 = gstore1, gstore2 = gstore3, gstore4 = gstore3, remove-refsize0(gstore1) = gstore1, as ∩ range fi0 = ∅, elems nx ∩ jro = ∅, dom gstore1 ∪ elems nx = dom gstore3 ∪ jro, fi2.inos < pmaxino, fi1.inos < jmaxino, p_os < pmaxino, gstore =○refsize gstore4, inv(gstore1), inv(gstore3 \ jro), inv-journal(nx, gstore, gstore0, jro), refsize-cons(gstore, range fi0 ∪ as), refsize-cons(gstore1, range fi2), refsize-cons(gstore3, range fi1), ri-inj(fi2), ri-inj(fi1), ri-inj(fi1 \ datakeys(key, n0, fi1)), adr ∈ as, pmaxino ≤ jmaxino, as.lebs ⊆ dom gstore, fi2.lebs ⊆ dom gstore1, fi1.lebs ⊆ dom gstore3, jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro) ⊦ ⟪index_get_gblock_refsize#(adr.lnum, fi0, fi, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; ; n); index_set_gblock_refsize#(adr.lnum, n - adr.size, fi0, fi, jro, gstore0, nx, pmaxino, p_os, jvalid; gstore); as := as -- adr⟫ ( ( (jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ dom gstore = dom gstore4 ∧ as ∩ range fi0 = ∅ ∧ as.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi0 ∪ as) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ gstore =○refsize gstore4) ∧ # as < # as0), as = ∅, pmaxino = 0, dups(nx)
jvalid0 ↔ jvalid2, as = as0, as1 = fi1[datakeys(key, n, fi1)], dom gstore = dom gstore4, fi = fi2, fi0 = fi1 \ datakeys(key, n, fi1), gstore0 = gstore1, gstore2 = gstore3, gstore4 = gstore3, remove-refsize0(gstore1) = gstore1, as ∩ range fi0 = ∅, elems nx ∩ jro = ∅, dom gstore1 ∪ elems nx = dom gstore3 ∪ jro, fi2.inos < pmaxino, fi1.inos < jmaxino, p_os < pmaxino, gstore =○refsize gstore4, inv(gstore1), inv(gstore3 \ jro), inv-journal(nx, gstore, gstore0, jro), refsize-cons(gstore, range fi0 ∪ as), refsize-cons(gstore1, range fi2), refsize-cons(gstore3, range fi1), ri-inj(fi2), ri-inj(fi1), ri-inj(fi1 \ datakeys(key, n, fi1)), pmaxino ≤ jmaxino, as.lebs ⊆ dom gstore, fi2.lebs ⊆ dom gstore1, fi1.lebs ⊆ dom gstore3, jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro) ⊦ as = ∅, pmaxino = 0, dups(nx), ∃ n, adr. adr ∈ as