[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, nonnull, disj-swap, disj-r, in-write-strong, disj, uni-com,
uni-emp-lprovedall subs proved uni-emp, disj-emp-r, uni-com,
uni-assprovedall subs proved disj-r, disj-l, at-uni, disj-distr-uni, disj-swap, 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-l, disj-r, at-uni, disj-swap, in-uni, ext,
del-uniprovedall subs proved disj-r, disj-l, disj, at-uni, at-del, in-uni, in-del, ext,
uni-injprovedall subs proved disj-r, disj-l, at-uni, in-uni, ext,
disj-distr-uniprovedall subs proved in-uni, disj,
at-uniprovedall subs proved disj-r, size-alloc, size-write, disj-l, at-alloc, nonnull, at-write, in-write-strong, uni-alloc, uni-write, in-alloc, disj-write, disj-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, in-alloc, disj-write, disj-alloc, sanity, exin, in-emp, ext, size-emp, uni-emp-r,
exin-uniprovedall subs proved in-write-strong, disj-write, in-uni, uni-emp-r, uni-alloc, disj-r, disj-emp-r, disj, in-alloc, in-emp, uni-write, sanity, exin, nonnull,
disj-diffprovedall subs proved diff-in, disj,
disj-swapprovedall subs proved disj-com-rw,
diff-atprovedall subs proved at-del, in-del, size-alloc, size-write, in-write-strong, diff-alloc, diff-write, in-alloc, sanity, exin, in-emp, ext, diff-emp,
disj-comprovedall subs proved disj-com-rw,
diff-inprovedall subs proved in-del, size-alloc, size-write, in-write-strong, diff-alloc, diff-write, in-alloc, sanity, exin, ext, in-emp, diff-emp,
in-uniprovedall subs proved size-alloc, size-write, uni-alloc, in-write-strong, uni-write, in-alloc, disj-write, disj-alloc, sanity, exin, ext, in-emp, uni-emp-r,
delswrprovedall subs proved diffs-sw, write-del, diffs-ins,
sw-del-add-01provedall subs proved sw-del-add,
sw-delswrprovedall subs proved in-del, sw-delwr, diffs-ins, diffs-emp,
write-delprovedall subs proved at-write, at-del, in-write-strong, in-del, ext,
disj-com-rwprovedall subs proved disj-l, disj,
disj-writeprovedall subs proved nonnull, disj-l, in-write-strong, in-alloc, disj,
disj-allocprovedall subs proved disj-l, in-alloc, disj,
exinprovedall subs proved at-del, at-alloc, at-write, ext, in-del, nonnull, in-write-strong, in-alloc,
sw-del-addprovedall subs proved at-alloc, at-del, at-write, in-write-strong, in-del, in-alloc, ext,
sw-delwrprovedall subs proved at-write, at-del, in-write-strong, in-del, ext,
write-twiceprovedall subs proved at-write, in-write-strong, ext,
write-againprovedall subs proved at-write, in-write-strong, ext,
sw-putprovedall subs proved at-write, in-write-strong, ext,
sw-del-add-newprovedall subs proved at-alloc, nonnull, at-diffs, at-write, in-write-strong, in-alloc, in-diffs, ext,
sw-alloc-putprovedall subs proved at-alloc, at-write, in-write-strong, in-alloc, ext,
overwriteprovedall subs proved at-write, in-write-strong, ext,
alloc-writeprovedall subs proved at-alloc, at-write, in-write-strong, in-alloc, ext,
diffs-swprovedall subs proved at-diffs, at-del, in-del, in-diffs, ext,
disj-lprovedall subs proved disj-r,
in-write-strongprovedall subs proved nonnull, in-write,
diffs-twiceprovedall subs proved at-diffs, in-diffs, ext,
subset-empprovedall subs proved ext, in-emp, subset, emp-subset,
write-rightprovedall subs proved uni-write, nonnull,
uni-emp-rprovedall subs proved uni-emp,
emp-subsetprovedall subs proved in-emp, subset,
subset-atprovedall subs proved subset,
subset-inprovedall subs proved subset,
at-diffsprovedall subs proved at-del, in-del, diffs-ins, diffs-emp,
in-diffsprovedall subs proved in-del, diffs-ins, diffs-emp,
disj-emp-rprovedall subs proved in-emp, disj,
disj-rprovedall subs proved disj,
nonnullprovedall subs proved sanity,
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,
uni-empaxiom
size-empaxiom
in-writeaxiom
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-allocaxiom
at-writeaxiom
at-allocaxiom