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

# lpt0 = # lpt, # avol0 = # lpt, (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gndx0, lax0, (n ∈ gstore0 ⊃ m11;0));groupblock(gndx1, lax2, m11)) = groupblock(gndx, lax, m), n < # lpt ∧ lpf1 = LP_GROUP_NODES ↔ n ∈ gstore, n < # lpt ∧ lpf1 = LP_INDEX_NODES ↔ n ∈ istore, n ∈ gstore0 ∨ n ∈ nx ↔ n ∈ gstore ∨ n ∈ ginval, lpt0[n] = mklp(m13, m14, lpf2, m15), istore[n] = indexblock(indx, lax1, m10), lpt[bleb.leb] = mklp(m3, m4, lpf0, m5), replay-lpt(lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx)), nx, # lpt)[n] = mklp(m0, m1, lpf, m2), gstore[n] = groupblock(gndx0, lax0, m6), lpt[n] = mklp(m7, m8, lpf1, m9), gstore0[n] = groupblock(gndx1, lax2, m11), istore0[n] = indexblock(indx0, lax3, m12), crash(gstore, gstore0, ginval, nx)[n] = groupblock(gndx2, lax4, m16), dom istore ∩ elems nx = ∅, ginval < # lpt, awbuf-inv(avol0, bleb), synced(avol0), avol1 ↓ avol0, istore0 ⊑ istore, n ∈ istore → avol0[n].mapped? ∧ abs-nodes(avol0[n].data, indx, lax1, m8 = LEB_SIZE) ∧ (m8 ≠ LEB_SIZE → m8 = # avol0[n].data) ∧ m7 = m10, n < # lpt → (n ∈ istore0 ↔ lpf2 = LP_INDEX_NODES ∧ m13 ≠ 0) ∧ (n ∈ gstore0 ↔ lpf2 = LP_GROUP_NODES ∧ m13 ≠ 0) ∧ (n ∈ istore0 → m13 = m12) ∧ (n ∈ gstore0 → m13 = m11) ∧ (lpf2 = LP_FREE → m13 = 0), 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. 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 < # lpt ∧ lpf = LP_GROUP_NODES ↔ n ∈ gstore ∨ n ∈ ginval) ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → avol1[n].mapped? ∧ abs-nodes(avol1[n].data, gndx2, lax4, m1 = LEB_SIZE) ∧ (m1 ≠ LEB_SIZE → m1 = # avol1[n].data)) ∧ (n ∈ gstore ∨ n ∈ ginval → m0 = m)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 46:
m < n, n ≤ # lpt ⊦ replay-lpt(lpt, nx, n)[m] = (lpt[m].flags = LP_FREE ∨ m ∈ nx ⊃ lpt[m] ;(lpt[m].flags = LP_INDEX_NODES ∧ lpt[m].ref-size ≠ 0 ⊃ lpt[m].size:= LEB_SIZE ;(lpt[m].ref-size = 0 ⊃ mklp(0, 0, LP_FREE, lpt[m].gcheapidx);lpt[m]) ) )
Proof step 47:
# avol0 = # lpt, # lpt0 = # lpt, (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gndx0, lax0, (n ∈ gstore0 ⊃ m11;0));groupblock(gndx1, lax2, m11)) = groupblock(gndx, lax, m), n ∈ gstore0 ∨ n ∈ nx ↔ n ∈ gstore ∨ n ∈ ginval, n < # lpt ∧ lpf1 = LP_INDEX_NODES ↔ n ∈ istore, n < # lpt ∧ lpf1 = LP_GROUP_NODES ↔ n ∈ gstore, crash(gstore, gstore0, ginval, nx)[n] = groupblock(gndx2, lax4, m16), istore0[n] = indexblock(indx0, lax3, m12), gstore0[n] = groupblock(gndx1, lax2, m11), lpt[n] = mklp(m7, m8, lpf1, m9), gstore[n] = groupblock(gndx0, lax0, m6), replay-lpt(lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx)), nx, # lpt)[n] = mklp(m0, m1, lpf, m2), lpt[bleb.leb] = mklp(m3, m4, lpf0, m5), istore[n] = indexblock(indx, lax1, m10), lpt0[n] = mklp(m13, m14, lpf2, m15), dom istore ∩ elems nx = ∅, ginval < # lpt, awbuf-inv(avol0, bleb), synced(avol0), avol1 ↓ avol0, istore0 ⊑ istore, 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, n < # lpt → (n ∈ istore0 ↔ lpf2 = LP_INDEX_NODES ∧ m13 ≠ 0) ∧ (n ∈ gstore0 ↔ lpf2 = LP_GROUP_NODES ∧ m13 ≠ 0) ∧ (n ∈ istore0 → m13 = m12) ∧ (n ∈ gstore0 → m13 = m11) ∧ (lpf2 = LP_FREE → m13 = 0), n ∈ istore → avol0[n].mapped? ∧ abs-nodes(avol0[n].data, indx, lax1, m8 = LEB_SIZE) ∧ (m8 ≠ LEB_SIZE → m8 = # avol0[n].data) ∧ m7 = m10, ∀ 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, bleb = nobuffer ∨ bleb.leb < # lpt ∧ (nx ≠ [] ∧ bleb.leb = nx.last ∧ lpf0 = LP_GROUP_NODES ∨ lpf0 = LP_INDEX_NODES) ⊦ (n < # lpt ∧ lpf = LP_GROUP_NODES ↔ n ∈ gstore ∨ n ∈ ginval) ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → avol1[n].mapped? ∧ abs-nodes(avol1[n].data, gndx2, lax4, m1 = LEB_SIZE) ∧ (m1 ≠ LEB_SIZE → m1 = # avol1[n].data)) ∧ (n ∈ gstore ∨ n ∈ ginval → m0 = m), n < # lpt ∧ # lpt ≤ # lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))
Proof step 51:
# avol0 = # lpt, # lpt0 = # lpt, (lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n].flags = LP_FREE ∨ n ∈ nx ⊃ lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n] ;( lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n].flags = LP_INDEX_NODES ∧ lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n].ref-size ≠ 0 ⊃ lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n].size:= LEB_SIZE ;(lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n].ref-size = 0 ⊃ mklp(0, 0, LP_FREE, lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n].gcheapidx) ;lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx))[n] ) ) ) = 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 ∈ gstore0 ∨ n ∈ nx ↔ n ∈ gstore ∨ n ∈ ginval, n < # lpt ∧ lpf1 = LP_INDEX_NODES ↔ n ∈ istore, n < # lpt ∧ lpf1 = LP_GROUP_NODES ↔ n ∈ gstore, crash(gstore, gstore0, ginval, nx)[n] = groupblock(gndx2, lax4, m16), istore0[n] = indexblock(indx0, lax3, m12), 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), istore[n] = indexblock(indx, lax1, m10), lpt0[n] = mklp(m13, m14, lpf2, m15), dom istore ∩ elems nx = ∅, ginval < # lpt, n < # lpt, awbuf-inv(avol0, bleb), synced(avol0), avol1 ↓ avol0, # lpt ≤ # lpt0.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx)), istore0 ⊑ istore, 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, n < # lpt → (n ∈ istore0 ↔ lpf2 = LP_INDEX_NODES ∧ m13 ≠ 0) ∧ (n ∈ gstore0 ↔ lpf2 = LP_GROUP_NODES ∧ m13 ≠ 0) ∧ (n ∈ istore0 → m13 = m12) ∧ (n ∈ gstore0 → m13 = m11) ∧ (lpf2 = LP_FREE → m13 = 0), n ∈ istore → avol0[n].mapped? ∧ abs-nodes(avol0[n].data, indx, lax1, m8 = LEB_SIZE) ∧ (m8 ≠ LEB_SIZE → m8 = # avol0[n].data) ∧ m7 = m10, ∀ 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, bleb = nobuffer ∨ bleb.leb < # lpt ∧ (nx ≠ [] ∧ bleb.leb = nx.last ∧ lpf0 = LP_GROUP_NODES ∨ lpf0 = LP_INDEX_NODES) ⊦ (n < # lpt ∧ lpf = LP_GROUP_NODES ↔ n ∈ gstore ∨ n ∈ ginval) ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → avol1[n].mapped? ∧ abs-nodes(avol1[n].data, gndx2, lax4, m1 = LEB_SIZE) ∧ (m1 ≠ LEB_SIZE → m1 = # avol1[n].data)) ∧ (n ∈ gstore ∨ n ∈ ginval → m0 = m)

Rule argument

spec: <toplevel> name: replay-lpt-at seq: m < n, n ≤ # lpt ⊦ replay-lpt(lpt, nx, n)[m] = (lpt[m].flags = LP_FREE ∨ m ∈ nx ⊃ lpt[m] ;(lpt[m].flags = LP_INDEX_NODES ∧ lpt[m].ref-size ≠ 0 ⊃ lpt[m].size:= LEB_SIZE ;(lpt[m].ref-size = 0 ⊃ mklp(0, 0, LP_FREE, lpt[m].gcheapidx) ;lpt[m] ) ) ) subst: [m, n, nx, lpt] → [n, # lpt, nx, lpt0 .mapIndices (elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx) )] flags: <all paths>

Additional information

Used terms: n, # lpt, nx, lpt0 .mapIndices (elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx) )