[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 142 from proof refine-commit (previous step)

# lpt1 = # avol0, # lpt = # avol0, # avol = # avol0, # lpt2 = # avol0, # lpt0 = # avol0, lpf = LP_GROUP_NODES ↔ n ∈ gstore2, lpt2[n] = mklp(m1, m2, lpf, m3), remove-refsize0(istore2)[n] = indexblock(indx, lax, m), remove-refsize0(gstore2)[n] = groupblock(gndx, lax0, m0), istore2[n] = indexblock(indx0, lax1, m4), gstore2[n] = groupblock(gndx0, lax2, m5), keyset(gch1) = gc-heap(cleanup-lpt(lpt), []), keyset(gch0) = gc-heap(lpt2, []), keyset(gch) = gc-heap(lpt2, log1), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, elems log1 ∩ ginval = ∅, dom remove-refsize0(gstore2) ∩ ginval = ∅, dom gstore1 ∪ elems log1 = dom gstore2 ∪ ginval, n < # avol0, ginval < # avol0, avol-cleanup-lpt-unchanged(avol, avol0, lpt), awbuf-inv(avol0, nobuffer), awbuf-inv(avol, nobuffer), awbuf-inv(avol, bleb0), bin-heap-inv(gch1, lpt1), bin-heap-inv(gch0, lpt), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb0, lpt2, avol), bufs-log-only(bleb0, log1, lpt2), freelist-cons(cleanup-lpt(lpt), freelist0), freelist-cons(lpt2, freelist), id-idx(cleanup-lpt(lpt), lpt1), id-idx(lpt2, lpt), inv(gstore2 \ ginval), inv(gstore1), inv(istore2), inv(istore1), log-group-block(log1, lpt2), lpt-free-unref(lpt2), lpt-free-unref(lpt0), lpt-leb-size(cleanup-lpt(lpt)), lpt-leb-size(lpt0), lpt-leb-size(lpt2), lpt-ram-flash(lpt1, lpt2, []), lpt-ram-flash(lpt2, lpt0, log1), synced(avol0), synced(avol), istore1 ⊑ istore2, n ∈ gstore2 → m1 = m5, n ∈ gstore2 ∧ ¬ n ∈ ginval → abs-leb(avol[n], groupblock(gndx0, lax2, m5), mklp(m1, m2, lpf, m3)), pstate = unbuffered → bleb0 = nobuffer, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore2, pstate.index? → pstate.lnum ∈ istore2, pstate ≠ unbuffered → bleb0 = buffered(pstate.lnum), n ∈ log1 → n ∈ gstore2, ∀ n. (n < # avol0 ∧ lpt2[n].flags = LP_INDEX_NODES ↔ n ∈ istore2) ∧ (n ∈ istore2 → abs-leb(avol[n], istore2[n], lpt2[n]) ∧ lpt2[n].ref-size = istore2[n].ref-size), ∀ n. n < # avol0 → (n ∈ istore1 ↔ lpt0[n].flags = LP_INDEX_NODES ∧ lpt0[n].ref-size ≠ 0) ∧ (n ∈ gstore1 ↔ lpt0[n].flags = LP_GROUP_NODES ∧ lpt0[n].ref-size ≠ 0) ∧ (n ∈ istore1 → lpt0[n].ref-size = istore1[n].ref-size) ∧ (n ∈ gstore1 → lpt0[n].ref-size = gstore1[n].ref-size) ∧ (lpt0[n].flags = LP_FREE → lpt0[n].ref-size = 0) ⊦ pstate = readonly, dups(log1), (n ∈ istore2 ∧ m4 ≠ 0 ↔ lpf = LP_INDEX_NODES ∧ m1 ≠ 0) ∧ (n ∈ gstore2 → (m5 ≠ 0 ↔ m1 ≠ 0)) ∧ (n ∈ istore2 ∧ m4 ≠ 0 → m1 = m) ∧ (n ∈ gstore2 ∧ m5 ≠ 0 → m1 = m0) ∧ (lpf = LP_FREE → m1 = 0)

User applied rule all left

And obtained the following new goals

Proof step 143:
# lpt0 = # avol0, # lpt2 = # avol0, # avol = # avol0, # lpt = # avol0, # lpt1 = # avol0, lpf = LP_GROUP_NODES ↔ n ∈ gstore2, n < # avol0 ∧ lpt2[n].flags = LP_INDEX_NODES ↔ n ∈ istore2, gstore2[n] = groupblock(gndx0, lax2, m5), istore2[n] = indexblock(indx0, lax1, m4), remove-refsize0(gstore2)[n] = groupblock(gndx, lax0, m0), remove-refsize0(istore2)[n] = indexblock(indx, lax, m), lpt2[n] = mklp(m1, m2, lpf, m3), keyset(gch) = gc-heap(lpt2, log1), keyset(gch0) = gc-heap(lpt2, []), keyset(gch1) = gc-heap(cleanup-lpt(lpt), []), remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, dom remove-refsize0(gstore2) ∩ ginval = ∅, elems log1 ∩ ginval = ∅, dom gstore1 ∪ elems log1 = dom gstore2 ∪ ginval, ginval < # avol0, n < # avol0, avol-cleanup-lpt-unchanged(avol, avol0, lpt), awbuf-inv(avol, bleb0), awbuf-inv(avol, nobuffer), awbuf-inv(avol0, nobuffer), bin-heap-inv(gch, lpt2), bin-heap-inv(gch0, lpt), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(false, bleb0, lpt2, avol), bufs-log-only(bleb0, log1, lpt2), freelist-cons(lpt2, freelist), freelist-cons(cleanup-lpt(lpt), freelist0), id-idx(lpt2, lpt), id-idx(cleanup-lpt(lpt), lpt1), inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval), log-group-block(log1, lpt2), lpt-free-unref(lpt0), lpt-free-unref(lpt2), lpt-leb-size(lpt2), lpt-leb-size(lpt0), lpt-leb-size(cleanup-lpt(lpt)), lpt-ram-flash(lpt2, lpt0, log1), lpt-ram-flash(lpt1, lpt2, []), synced(avol), synced(avol0), istore1 ⊑ istore2, n ∈ log1 → n ∈ gstore2, pstate ≠ unbuffered → bleb0 = buffered(pstate.lnum), pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore2, pstate = unbuffered → bleb0 = nobuffer, n ∈ gstore2 ∧ ¬ n ∈ ginval → abs-leb(avol[n], groupblock(gndx0, lax2, m5), mklp(m1, m2, lpf, m3)), n ∈ gstore2 → m1 = m5, n ∈ istore2 → abs-leb(avol[n], istore2[n], lpt2[n]) ∧ lpt2[n].ref-size = istore2[n].ref-size, ∀ n. n < # avol0 → (n ∈ istore1 ↔ lpt0[n].flags = LP_INDEX_NODES ∧ lpt0[n].ref-size ≠ 0) ∧ (n ∈ gstore1 ↔ lpt0[n].flags = LP_GROUP_NODES ∧ lpt0[n].ref-size ≠ 0) ∧ (n ∈ istore1 → lpt0[n].ref-size = istore1[n].ref-size) ∧ (n ∈ gstore1 → lpt0[n].ref-size = gstore1[n].ref-size) ∧ (lpt0[n].flags = LP_FREE → lpt0[n].ref-size = 0) ⊦ pstate = readonly, dups(log1), (n ∈ istore2 ∧ m4 ≠ 0 ↔ lpf = LP_INDEX_NODES ∧ m1 ≠ 0) ∧ (n ∈ gstore2 → (m5 ≠ 0 ↔ m1 ≠ 0)) ∧ (n ∈ istore2 ∧ m4 ≠ 0 → m1 = m) ∧ (n ∈ gstore2 ∧ m5 ≠ 0 → m1 = m0) ∧ (lpf = LP_FREE → m1 = 0)

Rule argument

pos: left 57 terms: n abort: F discard: T computed: T

Additional information

Used terms: n