| # lpt0 = # avol, # lpt2 = # avol, gstore[n] = groupblock(gndx, lax, m3), lpt2[n] = mklp(m3, m1, LP_GROUP_NODES, m2), gstore[n0] = groupblock(gndx0, lax0, m), lpt2[n0] = mklp(m0, m4, lpf, m5), lpt2[n, mklp(0, 0, LP_FREE, m2)][n0] = mklp(m6, m7, lpf0, m8), keyset(gch) = gc-heap(lpt2, log1), keyset(gch0) = gc-heap(lpt2, log1) -- key-index(m3, n), remove-refsize0(istore1) = istore1, remove-refsize0(gstore0) = gstore0, elems log1 ∩ ginval = ∅, dom gstore0 ∪ elems log1 = dom gstore ∪ ginval, ginval < # avol, n < # avol, abs-istore(avol, lpt2, istore2), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt2), bin-heap-inv(gch0, lpt), buf-ro-rw-mode(false, bleb, lpt2, avol), bufs-log-only(bleb, log1, lpt2), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt2, freelist), id-idx(lpt2[n, mklp(0, 0, LP_FREE, m2)], lpt), inv(istore1), inv(istore2), inv(gstore0), inv(gstore \ ginval), log-group-block(log1, lpt2), lpt-free-unref(lpt0), lpt-free-unref(lpt2), lpt-leb-size(lpt0), lpt-leb-size(lpt2), lpt-ram-flash(lpt2, lpt0, log1), synced(avol), key-index(m3, n) ∈ gc-heap(lpt2, log1), n ∈ gstore0, n ∈ gstore, istore1 ⊑ istore2, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore, pstate = unbuffered → bleb = nobuffer, pstate ≠ unbuffered → bleb = buffered(pstate.lnum), ∀ n. (n < # avol ∧ lpt2[n].flags = LP_GROUP_NODES ↔ n ∈ gstore) ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → abs-leb(avol[n], gstore[n], lpt2[n])) ∧ (n ∈ gstore → lpt2[n].ref-size = gstore[n].ref-size) ⊦ # gc-heap(lpt2, log1) = 0, buffered(n) = bleb, gc-heap(lpt2, log1) = ∅, pstate = readonly, dups(log1), n ∈ log1, (n0 < # avol ∧ lpf0 = LP_GROUP_NODES ↔ n0 ≠ n ∧ n0 ∈ gstore) ∧ (n0 ≠ n ∧ n0 ∈ gstore ∧ ¬ n0 ∈ ginval → abs-leb(avol[n0], groupblock(gndx0, lax0, m), mklp(m0, m4, lpf, m5))) ∧ (n0 ≠ n ∧ n0 ∈ gstore → m0 = m) |
# lpt2 = # avol, # lpt0 = # avol, n0 < # avol ∧ lpt2[n0].flags = LP_GROUP_NODES ↔ n0 ∈ gstore, lpt2[n, mklp(0, 0, LP_FREE, m2)][n0] = mklp(m6, m7, lpf0, m8), lpt2[n0] = mklp(m0, m4, lpf, m5), gstore[n0] = groupblock(gndx0, lax0, m), lpt2[n] = mklp(m3, m1, LP_GROUP_NODES, m2), gstore[n] = groupblock(gndx, lax, m3), keyset(gch0) = gc-heap(lpt2, log1) -- key-index(m3, n), keyset(gch) = gc-heap(lpt2, log1), remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, elems log1 ∩ ginval = ∅, dom gstore0 ∪ elems log1 = dom gstore ∪ ginval, n < # avol, ginval < # avol, abs-istore(avol, lpt2, istore2), awbuf-inv(avol, bleb), bin-heap-inv(gch0, lpt), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb, lpt2, avol), bufs-log-only(bleb, log1, lpt2), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt2, freelist), id-idx(lpt2[n, mklp(0, 0, LP_FREE, m2)], lpt), inv(gstore \ ginval), inv(gstore0), inv(istore2), inv(istore1), log-group-block(log1, lpt2), lpt-free-unref(lpt2), lpt-free-unref(lpt0), lpt-leb-size(lpt2), lpt-leb-size(lpt0), lpt-ram-flash(lpt2, lpt0, log1), synced(avol), n ∈ gstore, n ∈ gstore0, key-index(m3, n) ∈ gc-heap(lpt2, log1), istore1 ⊑ istore2, pstate ≠ unbuffered → bleb = buffered(pstate.lnum), pstate = unbuffered → bleb = nobuffer, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore2, n0 ∈ gstore ∧ ¬ n0 ∈ ginval → abs-leb(avol[n0], gstore[n0], lpt2[n0]), n0 ∈ gstore → lpt2[n0].ref-size = gstore[n0].ref-size ⊦ # gc-heap(lpt2, log1) = 0, buffered(n) = bleb, gc-heap(lpt2, log1) = ∅, pstate = readonly, dups(log1), n ∈ log1, (n0 < # avol ∧ lpf0 = LP_GROUP_NODES ↔ n0 ≠ n ∧ n0 ∈ gstore) ∧ (n0 ≠ n ∧ n0 ∈ gstore ∧ ¬ n0 ∈ ginval → abs-leb(avol[n0], groupblock(gndx0, lax0, m), mklp(m0, m4, lpf, m5))) ∧ (n0 ≠ n ∧ n0 ∈ gstore → m0 = m)
Used terms: n0