[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 persistence-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-syncprovedall subs proved flush-padding-space-write, flush-padding-space-header, flush-padding-space-aligned, prepost-encode-padding, elim-mapped, elim-lp-upd-size, sync,
inv-add-gndsprovedall subs proved prepost-encode-group-nodes, elim-mapped, elim-lp-upd-size, add-gnds,
inv-commitprovedall subs proved prepost-cleanup-lpt, prepost-gcheap-add-log, commit,
inv-recoverprovedall subs proved elim-lp-upd-size, prepost-create-gcheap, prepost-create-freelist, prepost-replay-lpt, prepost-replay-log, recover,
inv-formatprovedall subs proved prepost-create-freelist, format,
prepost-encode-paddingprovedall subs proved encode-padding-node,
flush-padding-space-headerprovedall subs proved flush-padding-space-aligned,
flush-padding-space-writeprovedall subs proved elim-mapped,
prepost-encode-group-nodesprovedall subs proved encode-group-nodes,
prepost-gcheap-add-logprovedall subs proved heap-add-log,
prepost-cleanup-lptprovedall subs proved id-idx-cleanup-lpt-backwards-fwd, nat-stuff0, elim-lp-upd-size, cleanup-lpt,
prepost-replay-logprovedall subs proved elim-lp-upd-size, replay-log,
prepost-replay-lptprovedall subs proved nat-stuff0, elim-lp-upd-size, replay-lpt,
prepost-create-gcheapprovedall subs proved nat-stuff0, create-gcheap,
prepost-create-freelistprovedall subs proved create-freelist,
inv-get-leb-sizeprovedall subs proved get-leb-size,
inv-is-readonlyprovedall subs proved is-readonly,
inv-is-log-emptyprovedall subs proved is-log-empty,
inv-get-block-free-sizeprovedall subs proved get-block-free-size,
inv-read-indprovedall subs proved read-ind, elim-mapped,
inv-read-gndprovedall subs proved read-gnd, elim-mapped,
inv-set-iblock-refsizeprovedall subs proved set-iblock-refsize,
inv-get-iblock-refsizeprovedall subs proved get-iblock-refsize,
inv-set-gblock-refsizeprovedall subs proved set-gblock-refsize,
inv-get-gblock-refsizeprovedall subs proved get-gblock-refsize,
inv-get-gc-blockprovedall subs proved get-gc-block,
inv-allocate-gndprovedall subs proved elim-lp-upd-size, allocate-leb, allocate-gnd,
inv-allocate-indprovedall subs proved elim-lp-upd-size, allocate-leb, allocate-ind,
inv-deallocate-gndprovedall subs proved elim-lp-upd-size, deallocate-gnd,
inv-requires-commitprovedall subs proved requires-commit,
inv-add-indprovedall subs proved elim-mapped, elim-lp-upd-size, add-ind,
inv-read-gblock-nodesprovedall subs proved range-eq-validtrailer, nat-stuff0, read-gblock-nodes, elim-mapped,
replay-lptaxiom
replay-logaxiom
heap-add-logaxiom
encode-padding-nodeaxiom
encode-group-nodesaxiom
create-gcheapaxiom
create-freelistaxiom
cleanup-lptaxiom
id-idx-cleanup-lpt-backwards-fwdprovedall subs proved
get-leb-sizeaxiom
is-readonlyaxiom
is-log-emptyaxiom
get-block-free-sizeaxiom
syncaxiom
flush-padding-space-alignedprovedall subs proved
add-gndsaxiom
read-indaxiom
read-gndaxiom
commitaxiom
recoveraxiom
set-iblock-refsizeaxiom
get-iblock-refsizeaxiom
set-gblock-refsizeaxiom
get-gblock-refsizeaxiom
get-gc-blockaxiom
allocate-gndaxiom
allocate-indaxiom
allocate-lebaxiom
deallocate-gndaxiom
requires-commitaxiom
formataxiom
add-indaxiom
elim-lp-upd-sizeprovedall subs proved
elim-mappedprovedall subs proved
read-gblock-nodesaxiom
nat-stuff0provedall subs proved
range-eq-validtrailerprovedall subs proved