[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 gjournal-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-gcprovedall subs proved inv-gc-copy, prepost-gc-referenced-nodes, gc,
inv-gc-copyprovedall subs proved abs-log-simp0, inv-gc-update-index, inv-addn, prepost-split-nodes, gc-copy,
inv-add5provedall subs proved inv-addn, add5,
inv-add1provedall subs proved inv-addn, add1,
inv-add2provedall subs proved inv-addn, add2,
inv-add3provedall subs proved inv-addn, add3,
inv-add4provedall subs proved inv-addn, add4,
inv-recoverprovedall subs proved term-restore-log, recover,
inv-gc-update-indexprovedall subs proved store, inv-store, gc-update-index,
inv-addnprovedall subs proved lf-inv-append-sizes, ls-inv-prefix-app-prefixn, ls-inv-reduce-jnlhead, inv-allocate, inv-transaction, addn,
term-restore-logprovedall subs proved term-remove-nonend-blocks, restore-log,
term-remove-nonend-blocksprovedall subs proved remove-nonend-blocks,
inv-storeprovedall subs proved store,
prepost-split-nodesprovedall subs proved split-nodes,
inv-transactionprovedall subs proved transaction,
inv-allocateprovedall subs proved allocate,
prepost-gc-referenced-nodesprovedall subs proved lf-inv-append-sizes, abs-log-simp0, gc-referenced-nodes,
inv-syncprovedall subs proved sync,
inv-getprovedall subs proved get,
inv-orphans-removeprovedall subs proved orphans-remove,
inv-orphans-insertprovedall subs proved orphans-insert,
inv-orphans-containsprovedall subs proved orphans-contains,
inv-commitprovedall subs proved commit,
inv-check-commitprovedall subs proved commit, check-commit,
inv-entriesprovedall subs proved entries,
inv-truncateprovedall subs proved remove-addresses, truncate,
inv-removeprovedall subs proved remove,
inv-lookupprovedall subs proved lookup,
inv-containsprovedall subs proved contains,
inv-newinoprovedall subs proved newino,
inv-formatprovedall subs proved format,
restore-logaxiom
remove-nonend-blocksaxiom
split-nodesaxiom
gc-referenced-nodesaxiom
add5axiom
syncaxiom
gc-update-indexaxiom
gc-copyaxiom
abs-log-simp0provedall subs proved
allocateaxiom
transactionaxiom
addnaxiom
ls-inv-reduce-jnlheadprovedall subs proved
ls-inv-prefix-app-prefixnprovedall subs proved
lf-inv-append-sizesprovedall subs proved
getaxiom
add1axiom
add2axiom
add3axiom
add4axiom
orphans-removeaxiom
orphans-insertaxiom
orphans-containsaxiom
check-commitaxiom
commitaxiom
recoveraxiom
gcaxiom
entriesaxiom
truncateaxiom
remove-addressesaxiom
removeaxiom
storeaxiom
lookupaxiom
containsaxiom
newinoaxiom
formataxiom