[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 17 from proof inv-write-vidhdr (
previous step
)
mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad, pebs[m].fill ≤ m0, m0 + n ≤ PEB_SIZE, n0 + n ≤ # buf, is-aligned(m0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE) ⊦ ⟪mtd_asm_write#(m, m0, n0, n, buf; pebs; err)⟫ mtd-cons(pebs)
A spec-lemma