[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 150 from proof recovery (
previous step
)
⊦ n < m ∧ m ≤ # ebatbl → absf(v, evol, apebs, ebatbl, q, m)[n] = (ebatbl[n] = unmapped ⊃ (v × n ∈ q.lebrefs ⊃ unmapped;erased) ;mapped(apebs[ebatbl[n].pnum].data, (evol[n].mapped? ⊃ evol[n].fill;apebs[ebatbl[n].pnum].fill)) )
A spec-lemma