[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 76 from proof abs-gstore-crash (previous step)

# avol0 = # lpt, # lpt0 = # lpt, # avol1 = # lpt, (n ∈ nx ⊃ mklp(m17, m18, lpf3, m19);(m17 = 0 ⊃ mklp(0, 0, LP_FREE, m19);mklp(m17, m18, lpf3, m19))) = mklp(m0, m1, lpf, m2), (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gndx0, lax0, (n ∈ gstore0 ⊃ m11;0));groupblock(gndx1, lax2, m11)) = groupblock(gndx, lax, m), (n ∈ nx ⊃ mklp(m13, LEB_SIZE, LP_GROUP_NODES, m15);mklp(m13, m14, lpf2, m15)) = mklp(m17, m18, lpf3, m19), n ∈ gstore0 ↔ lpf2 = LP_GROUP_NODES ∧ m13 ≠ 0, lpf1 = LP_GROUP_NODES ↔ n ∈ gstore, lpt0[n] = mklp(m13, m14, lpf2, m15), crash(gstore, gstore0, ginval, nx)[n] = groupblock(gndx2, lax4, m16), (∅)[n] = indexblock(indx, lax1, m10), gstore0[n] = groupblock(gndx1, lax2, m11), lpt[n] = mklp(m7, m8, lpf1, m9), gstore[n] = groupblock(gndx0, lax0, m6), lpt[bleb.leb] = mklp(m3, m4, lpf0, m5), dom istore ∩ elems nx = ∅, ginval < # lpt, n < # lpt, awbuf-inv(avol0, bleb), istore0 ⊑ istore, lpf2 = LP_FREE → m13 = 0, n ∈ gstore0 → m13 = m11, n ∈ gstore ∧ ¬ n ∈ ginval → avol0[n].mapped? ∧ abs-nodes(avol0[n].data, gndx0, lax0, m8 = LEB_SIZE) ∧ (m8 ≠ LEB_SIZE → m8 = # avol0[n].data), n ∈ gstore → m7 = m6, avol0[n].mapped? → avol1[n] = mapped(avol0[n].data.align↓), ¬ avol0[n].mapped? ∧ avol1[n].mapped? → # avol1[n].data ≤ LEB_SIZE ∧ is-aligned(# avol1[n].data, EB_PAGE_SIZE), ∀ n. n < # lpt ∧ avol0[n].mapped? → is-aligned(# avol0[n].data, EB_PAGE_SIZE), ∀ n. n < # lpt ∧ lpt0[n].flags = LP_FREE → lpt0[n].ref-size = 0, ∀ n. n < # lpt ∧ lpt0[n].flags = LP_GROUP_NODES ∧ lpt[n].flags = LP_GROUP_NODES ∧ ¬ n ∈ nx → lpt[n].size = lpt0[n].size, n ∈ gstore0 ∨ n ∈ nx, n ∈ gstore ∨ n ∈ ginval, bleb = nobuffer ∨ bleb.leb < # lpt ∧ (nx ≠ [] ∧ bleb.leb = nx.last ∧ lpf0 = LP_GROUP_NODES ∨ lpf0 = LP_INDEX_NODES) ⊦ lpf1 = LP_INDEX_NODES, lpf3 = LP_FREE, lpf3 = LP_INDEX_NODES, n ∈ istore, n ∈ istore0, lpf = LP_GROUP_NODES ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → avol1[n].mapped? ∧ abs-nodes(avol1[n].data, gndx2, lax4, m1 = LEB_SIZE) ∧ (m1 ≠ LEB_SIZE → m1 = # avol1[n].data)) ∧ m0 = m, lpf2 = LP_INDEX_NODES ∧ m13 ≠ 0

User applied rule all left

And obtained the following new goals

Proof step 77:
# avol1 = # lpt, # lpt0 = # lpt, # avol0 = # lpt, (n ∈ nx ⊃ mklp(m13, LEB_SIZE, LP_GROUP_NODES, m15);mklp(m13, m14, lpf2, m15)) = mklp(m17, m18, lpf3, m19), (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gndx0, lax0, (n ∈ gstore0 ⊃ m11;0));groupblock(gndx1, lax2, m11)) = groupblock(gndx, lax, m), (n ∈ nx ⊃ mklp(m17, m18, lpf3, m19);(m17 = 0 ⊃ mklp(0, 0, LP_FREE, m19);mklp(m17, m18, lpf3, m19))) = mklp(m0, m1, lpf, m2), lpf1 = LP_GROUP_NODES ↔ n ∈ gstore, n ∈ gstore0 ↔ lpf2 = LP_GROUP_NODES ∧ m13 ≠ 0, lpt[bleb.leb] = mklp(m3, m4, lpf0, m5), gstore[n] = groupblock(gndx0, lax0, m6), lpt[n] = mklp(m7, m8, lpf1, m9), gstore0[n] = groupblock(gndx1, lax2, m11), (∅)[n] = indexblock(indx, lax1, m10), crash(gstore, gstore0, ginval, nx)[n] = groupblock(gndx2, lax4, m16), lpt0[n] = mklp(m13, m14, lpf2, m15), dom istore ∩ elems nx = ∅, n < # lpt, ginval < # lpt, awbuf-inv(avol0, bleb), istore0 ⊑ istore, ¬ avol0[n].mapped? ∧ avol1[n].mapped? → # avol1[n].data ≤ LEB_SIZE ∧ is-aligned(# avol1[n].data, EB_PAGE_SIZE), avol0[n].mapped? → avol1[n] = mapped(avol0[n].data.align↓), n ∈ gstore → m7 = m6, n ∈ gstore ∧ ¬ n ∈ ginval → avol0[n].mapped? ∧ abs-nodes(avol0[n].data, gndx0, lax0, m8 = LEB_SIZE) ∧ (m8 ≠ LEB_SIZE → m8 = # avol0[n].data), n ∈ gstore0 → m13 = m11, lpf2 = LP_FREE → m13 = 0, n < # lpt ∧ avol0[n].mapped? → is-aligned(# avol0[n].data, EB_PAGE_SIZE), ∀ n. n < # lpt ∧ lpt0[n].flags = LP_GROUP_NODES ∧ lpt[n].flags = LP_GROUP_NODES ∧ ¬ n ∈ nx → lpt[n].size = lpt0[n].size, ∀ n. n < # lpt ∧ lpt0[n].flags = LP_FREE → lpt0[n].ref-size = 0, bleb = nobuffer ∨ bleb.leb < # lpt ∧ (nx ≠ [] ∧ bleb.leb = nx.last ∧ lpf0 = LP_GROUP_NODES ∨ lpf0 = LP_INDEX_NODES), n ∈ gstore ∨ n ∈ ginval, n ∈ gstore0 ∨ n ∈ nx ⊦ lpf1 = LP_INDEX_NODES, lpf3 = LP_INDEX_NODES, lpf3 = LP_FREE, n ∈ istore0, n ∈ istore, lpf2 = LP_INDEX_NODES ∧ m13 ≠ 0, lpf = LP_GROUP_NODES ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → avol1[n].mapped? ∧ abs-nodes(avol1[n].data, gndx2, lax4, m1 = LEB_SIZE) ∧ (m1 ≠ LEB_SIZE → m1 = # avol1[n].data)) ∧ m0 = m

Rule argument

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

Additional information

Used terms: n