| jvalid ↔ jvalid0, gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), fi2[key] = @(m3, m4, m5), gstore3[m3] = groupblock(gndx, lax, m6), fi = fi1, fi0 = fi2[key, @(m0, m1, m2)], gstore = gstore3, gstore0 = gstore2, gstore1 = gstore3, jro = jro0, lnum = m3, n = m6 - m5, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, jro1 < jmaxino, p_os < pmaxino, fi2.inos < jmaxino, fi1.inos < pmaxino, inv(gstore3 \ jro0), inv(gstore2), key-cons(key, nd), refsize-cons(gstore3, range fi2), refsize-cons(gstore2, range fi1), ri-inj(fi2), ri-inj(fi2[key, @(m0, m1, m2)]), ri-inj(fi1), key ∈ fi2, @(m0, m1, m2) ∈ gstore3, m3 ∈ gstore3, pmaxino ≤ jmaxino, m6 ≥ m5, fi2.lebs ⊆ dom gstore3, fi1.lebs ⊆ dom gstore2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ [if lnum ∈ gstore then gstore[lnum].ref-size := n else abort] ( inv(gstore \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore ∪ jro0 → ⟪index_get_gblock_refsize#(m0, fi2[key, @(m0, m1, m2)], fi1, jro0, gstore, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(m0, n + m2, fi2[key, @(m0, m1, m2)], fi1, jro0, gstore2, nx, pmaxino, p_os, jvalid0; gstore); jmaxino := max(key.ino + 1, jmaxino)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi2.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi2[key, @(m0, m1, m2)].lebs ⊆ dom gstore ∧ refsize-cons(gstore, (range fi2 -- fi2[key]) ++ @(m0, m1, m2)) ∧ inv(gstore \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore ∪ jro0 ∧ gstore =○refsize gstore1)), jmaxino = 0, pmaxino = 0, dups(nx), @(m0, m1, m2) ∈ fi2 |
jvalid ↔ jvalid0, gstore3[m3] = groupblock(gndx, lax, m6), fi2[key] = @(m3, m4, m5), gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), fi = fi1, fi0 = fi2[key, @(m0, m1, m2)], gstore = gstore3, gstore0 = gstore2, gstore1 = gstore3, jro = jro0, lnum = m3, n = m6 - m5, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, fi1.inos < pmaxino, fi2.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore2), inv(gstore3 \ jro0), key-cons(key, nd), refsize-cons(gstore2, range fi1), refsize-cons(gstore3, range fi2), ri-inj(fi1), ri-inj(fi2[key, @(m0, m1, m2)]), ri-inj(fi2), m3 ∈ gstore3, @(m0, m1, m2) ∈ gstore3, key ∈ fi2, pmaxino ≤ jmaxino, m6 ≥ m5, fi1.lebs ⊆ dom gstore2, fi2.lebs ⊆ dom gstore3, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ [gstore[lnum].ref-size := n] ( inv(gstore \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore ∪ jro0 → ⟪index_get_gblock_refsize#(m0, fi2[key, @(m0, m1, m2)], fi1, jro0, gstore, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(m0, n + m2, fi2[key, @(m0, m1, m2)], fi1, jro0, gstore2, nx, pmaxino, p_os, jvalid0; gstore); jmaxino := max(key.ino + 1, jmaxino)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi2.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi2[key, @(m0, m1, m2)].lebs ⊆ dom gstore ∧ refsize-cons(gstore, (range fi2 -- fi2[key]) ++ @(m0, m1, m2)) ∧ inv(gstore \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore ∪ jro0 ∧ gstore =○refsize gstore1)), jmaxino = 0, pmaxino = 0, dups(nx), @(m0, m1, m2) ∈ fi2