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

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