[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 78 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), 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 insert rewrite lemma

And obtained the following new goals

Proof step 79:
⊦ n ∈ crash(gstore, gstore0, ginval, nx) → crash(gstore, gstore0, ginval, nx)[n] = (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gstore[n].gndlist, gstore[n].ladrlist, (n ∈ gstore0 ⊃ gstore0[n].ref-size;0));gstore0[n])
Proof step 80:
# avol1 = # lpt, # lpt0 = # lpt, # avol0 = # lpt, (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gstore[n].gndlist, gstore[n].ladrlist, (n ∈ gstore0 ⊃ gstore0[n].ref-size;0));gstore0[n]) = groupblock(gndx2, lax4, m16), (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), lpt0[n] = mklp(m13, m14, lpf2, m15), dom istore ∩ elems nx = ∅, n < # lpt, ginval < # lpt, awbuf-inv(avol0, bleb), n ∈ crash(gstore, gstore0, ginval, nx), istore0 ⊑ istore, avol0[n].mapped? → is-aligned(# avol0[n].data, EB_PAGE_SIZE), ¬ 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. 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

spec: apersistence-base name: crash-group-at seq: ⊦ n ∈ crash(gstore, gstore0, ginval, nx) → crash(gstore, gstore0, ginval, nx)[n] = (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock (gstore[n].gndlist, gstore[n].ladrlist, (n ∈ gstore0 ⊃ gstore0[n].ref-size;0)) ;gstore0[n] ) subst: [n, nx, ginval, gstore0, gstore] → [n, nx, ginval, gstore0, gstore] flags: <all paths>

Additional information

Used simplifier rules: ⊦ ¬ n ∈ gstore → gstore[n] = (∅)[n]; (s)% ⊦ n ∈ crash(gstore, gstore0, ginval, nx) ↔ n ∈ gstore ∨ n ∈ ginval; (ws) Used terms: n, nx, ginval, gstore0, gstore