[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:
write-leftprovedall subs proved uni-write, disj-com-rw, nonnull, disj-r, in-write, disj, uni-com,
uni-emp-lprovedall subs proved uni-emp-r, disj-emp-r, uni-com,
uni-assprovedall subs proved disj-r, at-uni, disj-distr-uni, disj-com-rw, disj-distr-uni-com, in-uni, ext,
subset-uniprovedall subs proved disj-r, subset, disj, subset-at, diff-at, at-uni, subset-in, diff-in, in-uni, ext, uni-com,
disj-distr-uni-comprovedall subs proved disj-distr-uni, disj-com,
uni-comprovedall subs proved disj-r, disj-l, at-uni, disj-com-rw, in-uni, ext,
union-left-singleton-atprovedall subs proved at-write, nonnull, disj-singleton-write, in-alloc, in-emp, in-write, in-uni, at-uni,
union-left-singletonprovedall subs proved at-del, at-write, at-uni, in-alloc, in-emp, in-write, in-del, disj-singleton-write, in-uni, nonnull, ext,
uni-injprovedall subs proved disj-r, disj-l, at-uni, in-uni, ext,
del-uniprovedall subs proved disj-r, disj-l, disj, at-uni, at-del, in-uni, in-del, ext,
disj-distr-uniprovedall subs proved disj-r, disj-l, in-uni, disj,
at-uniprovedall subs proved disj-r, size-alloc, size-write, disj-l, at-alloc, in-write, uni-alloc, at-write, uni-write, disj-alloc, disj-write, in-alloc, sanity, exin, ext, in-emp, disj-emp-r, uni-emp-r, in-uni,
size-uniprovedall subs proved in-uni, uni-alloc, size-alloc, size-write, uni-write, disj-alloc, disj-write, in-alloc, sanity, exin, in-emp, ext, size-emp, uni-emp-r,
exin-uniprovedall subs proved in-write, disj-write, in-uni, uni-emp-r, uni-alloc, disj-emp-r, disj-r, disj, in-alloc, in-emp, uni-write, sanity, exin, nonnull,
disj-comprovedall subs proved disj-com-rw,
in-uniprovedall subs proved size-alloc, size-write, uni-alloc, in-write, uni-write, disj-alloc, disj-write, in-alloc, sanity, exin, ext, in-emp, uni-emp-r,
disj-diffprovedall subs proved diff-in, disj,
diff-atprovedall subs proved at-del, in-del, size-alloc, size-write, in-write, diff-alloc, diff-write, in-alloc, sanity, exin, in-emp, ext, diff-emp,
diff-inprovedall subs proved in-del, size-alloc, size-write, in-write, diff-alloc, diff-write, in-alloc, sanity, exin, ext, in-emp, diff-emp,
disj-com-rwprovedall subs proved disj-l, disj,
disj-writeprovedall subs proved nonnull, disj-l, in-alloc, in-write, disj,
disj-allocprovedall subs proved disj-l, in-alloc, disj,
delswrprovedall subs proved diffs-sw, write-del, diffs-ins,
diffs-swprovedall subs proved at-diffs, at-del, in-del, in-diffs, ext,
exinprovedall subs proved at-del, at-alloc, at-write, ext, in-del, nonnull, in-alloc, in-write,
disj-lprovedall subs proved disj-r,
write-rightprovedall subs proved uni-write, nonnull,
sw-delswrprovedall subs proved in-del, sw-delwr, diffs-ins, diffs-emp,
sw-del-add-newprovedall subs proved at-alloc, nonnull, at-diffs, at-write, in-alloc, in-write, in-diffs, ext,
sw-del-add-01provedall subs proved sw-del-add,
sw-alloc-putprovedall subs proved at-alloc, nonnull, at-write, in-alloc, in-write, ext,
subset-empprovedall subs proved ext, in-emp, subset, emp-subset,
diffs-twiceprovedall subs proved at-diffs, in-diffs, ext,
disj-singleton-writeprovedall subs proved in-alloc, in-emp, in-write, disj,
sw-delwrprovedall subs proved at-write, at-del, in-write, in-del, ext,
sw-del-addprovedall subs proved at-alloc, at-del, at-write, in-alloc, in-del, in-write, ext,
subset-inprovedall subs proved subset,
subset-atprovedall subs proved subset,
emp-subsetprovedall subs proved in-emp, subset,
nonnullprovedall subs proved sanity,
in-diffsprovedall subs proved in-del, diffs-ins, diffs-emp,
at-diffsprovedall subs proved at-del, in-del, diffs-ins, diffs-emp,
write-delprovedall subs proved at-write, at-del, in-write, in-del, ext,
uni-emp-rprovedall subs proved uni-emp,
disj-emp-rprovedall subs proved in-emp, disj,
disj-rprovedall subs proved disj,
write-againprovedall subs proved at-write, in-write, ext,
sw-putprovedall subs proved at-write, in-write, ext,
overwrite-split2provedall subs proved at-write, in-write, ext,
overwrite-splitprovedall subs proved at-write, in-write, ext,
overwrite-1provedall subs proved at-write, in-write, ext,
overwriteprovedall subs proved at-write, in-write, ext,
in-write-strongprovedall subs proved in-write,
disj-emp-lprovedall subs proved in-emp, disj,
del-twiceprovedall subs proved at-del, in-del, ext,
del-swprovedall subs proved at-del, in-del, ext,
del-notinprovedall subs proved at-del, in-del, ext,
del-newprovedall subs proved at-alloc, at-del, in-alloc, in-del, ext,
alloc-writeprovedall subs proved at-alloc, at-write, in-alloc, in-write, ext,
uni-empaxiom
size-empaxiom
subsetaxiom
diff-empaxiom
diff-writeaxiom
diff-allocaxiom
disjaxiom
in-empaxiom
sanityaxiom
uni-writeaxiom
uni-allocaxiom
size-writeaxiom
size-allocaxiom
diffs-empaxiom
diffs-insaxiom
in-delaxiom
at-delaxiom
extaxiom
in-writeaxiom
in-allocaxiom
at-writeaxiom
at-allocaxiom