[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 heap

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:
size-zeroprovedall subs proved size-alloc, size-write, in-alloc, sanity, exin, in-emp, ext, size-emp,
sw-del-add-01provedall subs proved sw-del-add,
rm-sizeprovedall subs proved size-alloc, size-write, in-alloc, del-new, write-del, sanity, exin,
structindprovedall subs proved size-alloc, size-write, in-alloc, sanity, exin, in-emp, ext,
write-delprovedall subs proved at-del, at-write-other, in-write, in-del, ext,
sw-del-addprovedall subs proved at-alloc, at-write-same-alloc, at-del, in-alloc, in-del, at-write, in-write, ext,
exinprovedall subs proved at-del, at-alloc, at-write, ext, in-del, nonnull, in-alloc, in-write,
at-write-mod-three-other-3provedall subs proved at-write-mod-other-2, at-write,
at-write-mod-two-otherprovedall subs proved at-write-mod-other, at-write,
at-write-mod-three-otherprovedall subs proved at-write-mod-other, at-write,
at-write-mod-two-other-3provedall subs proved at-write-mod-other-2, at-write,
del-newprovedall subs proved at-alloc, at-del, in-alloc, in-del, ext,
at-write-same-allocprovedall subs proved in-alloc, at-write,
nonnullprovedall subs proved sanity,
at-write-mod-otherprovedall subs proved at-write,
at-write-mod-other-2provedall subs proved in-write, at-write,
at-write-otherprovedall subs proved at-write,
del-swprovedall subs proved at-del, in-del, ext,
at-write-mod-three-other-4provedall subs proved in-write, at-write,
at-write-mod-three-other-2provedall subs proved in-write, at-write,
overwriteprovedall subs proved at-write, in-write, ext,
overwrite-splitprovedall subs proved at-write, in-write, ext,
write-againprovedall subs proved at-write, in-write, ext,
at-write-sameprovedall subs proved at-write,
sw-putprovedall subs proved at-write, in-write, ext,
sw-alloc-putprovedall subs proved at-write, at-alloc, in-write, in-alloc, ext,
del-notinprovedall subs proved at-del, in-del, ext,
sw-delwrprovedall subs proved at-del, in-del, at-write, in-write, ext,
overwrite-split2provedall subs proved at-write, in-write, ext,
in-write-strongprovedall subs proved in-write,
put-eqprovedall subs proved at-write, in-write, ext,
del-twiceprovedall subs proved at-del, in-del, ext,
at-write-mod-two-other-2provedall subs proved in-write, at-write,
alloc-writeprovedall subs proved at-write, at-alloc, in-write, in-alloc, ext,
size-empaxiom
in-empaxiom
sanityaxiom
size-writeaxiom
size-allocaxiom
at-allocaxiom
at-writeaxiom
in-allocaxiom
in-writeaxiom
extaxiom
in-delaxiom
at-delaxiom