[Imprint][Data Privacy Statement][E-Mail]

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,

Lemma dependency for Specification ubi-crash-recovery-base

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
vols-is-max-is-min-eraseqprovedall subs proved in-eraseq-strong-valid, vols-is-max-weak, vols-le, vols-is-max-is-max-vols,
vols-is-max-is-max-volsprovedall subs proved in-eraseq-strong-not-valid, valid-eraseq-strong-imp-p, valid-eraseq-strong-imp-q, ubi-cons-same-vtbl, vols-is-max-weak, vols-le,
valid-wl-map-indicesprovedall subs proved indices-erasing-at,
valid-vtbl-map-indices-erasingprovedall subs proved indices-erasing-at,
valid-eraseq-stronger-prev-append-lrefprovedall subs proved valid-eraseq-stronger-rec, valid-eraseq-stronger-one, valid-eraseq-stronger-base,
valid-eraseq-stronger-next-append-noneprovedall subs proved valid-eraseq-stronger-rec, valid-eraseq-stronger-base, valid-eraseq-stronger-one,
valid-eraseq-stronger-next-append-lrefprovedall subs proved valid-eraseq-stronger-rec, valid-eraseq-stronger-base, valid-eraseq-stronger-one,
ubi-io-initial-unique-sqnsprovedall subs proved ubi-io-initial-valid-sqns,
indices-erasing-write-prependprovedall subs proved indices-set-erasing, indices-erasing-rec,
in-eraseq-strong-validprovedall subs proved valid-eraseq-strong-rec,
valid-eraseq-strong-imp-qprovedall subs proved valid-eraseq-strong-rec, valid-eraseq-strong-base,
valid-eraseq-strong-imp-pprovedall subs proved valid-eraseq-strong-rec, valid-eraseq-strong-base,
in-eraseq-strong-not-validprovedall subs proved valid-eraseq-strong-rec,
indices-erasing-atprovedall subs proved indices-erasing-rec,
valid-eraseq-stronger-oneprovedall subs proved valid-eraseq-stronger-base, valid-eraseq-stronger-rec,
ubi-io-initial-valid-sqnsprovedall subs proved ubi-io-initial-valid-sqns-h,
indices-set-erasingprovedall subs proved indices-erasing-rec, indices-erasing-base,
vols-le-transprovedall subs proved vols-le,
vols-le-reflprovedall subs proved vols-le,
vols-le-antisymprovedall subs proved vols-le,
valid-recs-sqns-updateprovedall subs proved valid-recs-sqns,
valid-recs-sqns-emptysetprovedall subs proved valid-recs-sqns,
valid-recs-next-updateprovedall subs proved valid-recs,
valid-recs-next-samerecsprovedall subs proved valid-recs,
valid-recs-next-addprovedall subs proved valid-recs,
valid-recs-in-nonempty-sqnsprovedall subs proved valid-recs,
valid-recs-emptysetprovedall subs proved valid-recs,
valid-eraseq-stronger-no-maxsqnumprovedall subs proved valid-eraseq-stronger-rec,
valid-eraseq-stronger-nextprovedall subs proved valid-eraseq-stronger-rec, valid-eraseq-stronger-base,
valid-eraseq-stronger-imp-strongprovedall subs proved valid-eraseq-strong-rec, valid-eraseq-stronger-rec, valid-eraseq-strong-base, valid-eraseq-stronger-base,
valid-eraseq-strong-notinvolsprovedall subs proved valid-eraseq-strong-rec, valid-eraseq-strong-base,
unmapped-vols-unmappedprovedall subs proved unmapped-vols,
unmapped-vols-disjprovedall subs proved disj, unmapped-vols,
indices-erasing-write-notinprovedall subs proved indices-erasing-rec, indices-erasing-base,
indices-erasing-eraseqprovedall subs proved indices-erasing-rec, indices-erasing-base,
disj-shiftprovedall subs proved disj,
disj-removeprovedall subs proved disj,
vols-leaxiom
vols-is-max-weakaxiom
ubi-cons-same-vtblprovedall subs proved
valid-recs-sqnsaxiom
valid-recsaxiom
valid-eraseq-stronger-baseaxiom
valid-eraseq-stronger-recaxiom
valid-eraseq-strong-baseaxiom
unmapped-volsaxiom
ubi-io-initial-valid-sqns-hprovedall subs proved
indices-erasing-baseaxiom
indices-erasing-recaxiom
valid-eraseq-strong-recaxiom
disjaxiom