[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 aubifs-internal-asm

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:
inv-check-commitprovedall subs proved inv-commit, check-commit,
inv-commitprovedall subs proved commit,
inv-add5provedall subs proved add5,
crash-neutral-add5provedall subs proved add5,
inv-recoverprovedall subs proved recover,
crash-neutral-recoverprovedall subs proved recover,
crash-neutral-newinoprovedall subs proved newino,
crash-neutral-containsprovedall subs proved contains,
crash-neutral-lookupprovedall subs proved lookup,
crash-neutral-storeprovedall subs proved store,
crash-neutral-removeprovedall subs proved remove,
crash-neutral-truncateprovedall subs proved truncate,
crash-neutral-entriesprovedall subs proved entries,
crash-neutral-getprovedall subs proved get,
crash-neutral-add1provedall subs proved add1,
crash-neutral-add2provedall subs proved add2,
crash-neutral-add3provedall subs proved add3,
crash-neutral-add4provedall subs proved add4,
crash-neutral-gcprovedall subs proved gc-drop, gc-step, gc,
crash-neutral-check-commitprovedall subs proved check-commit,
crash-neutral-commitprovedall subs proved commit,
crash-neutral-orphans-containsprovedall subs proved orphans-contains,
crash-neutral-orphans-insertprovedall subs proved orphans-insert,
crash-neutral-orphans-removeprovedall subs proved orphans-remove,
inv-newinoprovedall subs proved newino,
inv-containsprovedall subs proved contains,
inv-lookupprovedall subs proved lookup,
inv-storeprovedall subs proved store,
inv-removeprovedall subs proved remove,
inv-truncateprovedall subs proved truncate,
inv-entriesprovedall subs proved entries,
inv-getprovedall subs proved get,
inv-add1provedall subs proved add1,
inv-add2provedall subs proved add2,
inv-add3provedall subs proved add3,
inv-add4provedall subs proved add4,
inv-gcprovedall subs proved gc-drop, gc-step, gc,
inv-orphans-containsprovedall subs proved orphans-contains,
inv-orphans-insertprovedall subs proved orphans-insert,
inv-orphans-removeprovedall subs proved orphans-remove,
crash-neutral-syncprovedall subs proved sync-01,
inv-syncprovedall subs proved sync-01,
inv-formatprovedall subs proved format,
add5axiom
recoveraxiom
newinoaxiom
containsaxiom
lookupaxiom
storeaxiom
removeaxiom
truncateaxiom
entriesaxiom
getaxiom
add1axiom
add2axiom
add3axiom
add4axiom
gcaxiom
gc-stepaxiom
gc-dropaxiom
check-commitaxiom
commitaxiom
orphans-containsaxiom
orphans-insertaxiom
orphans-removeaxiom
sync-01axiom
formataxiom