| gstore3[m0, groupblock(gndx, lax, m3 + m2)][n] = groupblock(gndx0, lax0, m4), gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), gstore3[m0] = groupblock(gndx, lax, m3), gstore3[n] = groupblock(gndx1, lax1, 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[m0, groupblock(gndx, lax, m3 + m2)] \ jro0), inv(gstore3 \ jro0), inv(gstore2), key-cons(key, nd), refsize-cons(gstore2, range fi1), ri-inj(fi2), ri-inj(fi2[key, @(m0, m1, m2)]), ri-inj(fi1), n ∈ gstore3[m0, groupblock(gndx, lax, m3 + m2)], m0 ∈ gstore3, @(m0, m1, m2) ∈ gstore3, pmaxino ≤ max(key.ino + 1, jmaxino), pmaxino ≤ jmaxino, fi2.lebs ⊆ dom gstore3, fi1.lebs ⊆ dom gstore2, n ∈ gstore3 → m5 = (range fi2 | n).size, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ jmaxino = 0, m4 = ((range fi2 ++ @(m0, m1, m2)) | n).size, max(key.ino + 1, jmaxino) = 0, pmaxino = 0, dups(nx), @(m0, m1, m2) ∈ fi2, key ∈ fi2 |
Used simplifier rules: ⊦ n ≠ n0 → gstore[n0, gblock][n] = gstore[n]; (s)%m ≠ m0 ⊦ (as ++ @(m0, m1, m2)) | m = as | m; (s)% ⊦ n ≠ n0 → (n ∈ gstore[n0, gblock] ↔ n ∈ gstore); (s)%⊦ groupblock(gndx, lax, m) = groupblock(gndx0, lax0, m0) ↔ gndx = gndx0 ∧ lax = lax0 ∧ m = m0; (ws)% ⊦ gstore[n, gblock][n] = gblock; (s)% ⊦ (as ++ @(m0, m1, m2)) | m0 = (as | m0) ++ @(m0, m1, m2); (s)% ⊦ (as ++ adr).size = (adr ∈ as ⊃ as.size;as.size + adr.size); (s)% ⊦ @(m, m0, m1) ∈ as | m ↔ @(m, m0, m1) ∈ as; (s)% ⊦ adr ∈ range ri ↔ adr ∈ ri; (s)% ⊦ @(m, m0, m1).size = m1; (s)% ⊦ n ∈ gstore[n, gblock]; (s) Used formulas: n = m0