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