| # ax3 = # ndx2, # ax2 = # ndx1, jvalid ↔ jvalid0, gstore3[@(m, m0, m1)] = mkgnode(nd, m2, boolvar, boolvar0), fi2[ndx2.keys, ax3][nd.key] = @(m3, m4, m5), abs-log(nx, gstore3 ↓) = abs-log(nx, gstore2 ↓), dom gstore3 = dom gstore2, fi = fi1, fi0 = fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)], gstore = gstore1, gstore0 = gstore3, jro = jro0, lnum = m3, nodes(gstore3 ↓, jro0) = nodes(gstore2 ↓, jro0), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, range fi2 ∩ ax2.toSet = ∅, range fi2 ∩ ax3.toSet = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, fi1.inos < pmaxino, fi2[ndx2.keys, ax3].inos < jmaxino, p_os < pmaxino, fi2.inos < jmaxino1, jro1 < jmaxino1, inv(gstore3 \ jro0), inv(gstore1), inv(gstore2 \ jro0), key-cons(nd.key, nd), key-cons(ndx2), key-cons(ndx1), nodes-cons(ax3 + @(m, m0, m1) ' + ax2, ndx2 + nd ' + ndx1, gstore2, jro0), nodes-cons(ax2, ndx1, gstore3, jro0), refsize-cons(gstore1, range fi1), refsize-cons(gstore3, range fi2[ndx2.keys, ax3]), refsize-cons(gstore2, range fi2), ri-inj(fi1), ri-inj(fi2), nd.key ∈ fi2[ndx2.keys, ax3], @(m, m0, m1) ∈ gstore3, nd.key ∈ fi2, m3 ∈ gstore2, pmaxino ≤ jmaxino, pmaxino ≤ jmaxino1, jmaxino1 ≤ jmaxino, fi1.lebs ⊆ dom gstore1, fi2[ndx2.keys, ax3].lebs ⊆ dom gstore2, ndx1.keys.toSet ⊆ dom fi2, fi2.lebs ⊆ dom gstore2, ndx2.keys.toSet ⊆ dom fi2, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ [abort; gstore := gstore3; index_set_gblock_refsize#(m3, n - m5, fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)], fi1, jro0, gstore1, nx, pmaxino, p_os, jvalid0; gstore3); index_get_gblock_refsize#(m, fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)], fi1, jro0, gstore3, gstore1, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(m, n + m1, fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)], fi1, jro0, gstore1, nx, pmaxino, p_os, jvalid0; gstore3); jmaxino := max(nd.key.ino + 1, jmaxino)] ( fi2[ndx2.keys, ax3].inos < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi2[ndx2.keys, ax3].inos ∪ (nd.key.inode? ⊃ ∅ ++ nd.key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0)) ∧ fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)].lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)]) ∧ inv(gstore3 \ jro0) ∧ dom gstore1 ∪ elems nx = dom gstore3 ∪ jro0 ∧ ri-inj(fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)]) ∧ gstore3 =○refsize gstore → ⟪ax0 := ax2; ndx0 := ndx1⟫ ( (∃ ax, ndx. # ax = # ndx ∧ ax3 + @(m, m0, m1) ' + ax2 = ax + ax0 ∧ ndx2 + nd ' + ndx1 = ndx + ndx0 ∧ fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)] = fi2[ndx.keys, ax]) ∧ (dom fi2 ∪ ndx2.keys.toSet) ++ nd.key = dom fi2 ∧ jmaxino1 ≤ jmaxino ∧ dom gstore3 = dom gstore2 ∧ nodes-cons(ax0, ndx0, gstore3, jro0) ∧ nodes(gstore ↓, jro0) = nodes(gstore2 ↓, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓) ∧ (jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0)) ∧ ¬ # ax2 < # ax0)), jmaxino = 0, jmaxino1 = 0, pmaxino = 0, dups(nx), dups(ax3 + ax2), dups(ax3), dups(ax2), m ∈ jro0, @(m, m0, m1) ∈ fi2, @(m, m0, m1) ∈ ax2, @(m, m0, m1) ∈ ax3, lnum ∈ gstore0 |