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

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:
union-split3provedall subs proved uni-ac3-true, uni-inj, uni-ass, disj-com-rw, union-split2, disj-distr-uni-com, disj-distr-uni,
union-split2provedall subs proved uni-ac3-true, uni-inj, uni-ass, uni-com, disj-diffb, subset-union2, disj-com-rw, disj-l, disj-r, diff-at, diff-in, at-uni, subset-union, disj-union-diff, in-uni, disj-distr-uni, disj-distr-uni-com,
subset-union33provedall subs proved subset-union32, disj-distr-uni, disj-com-rw, disj-distr-uni-com, uni-com,
subset-union32provedall subs proved subset-union31, disj-com-rw, uni-ass, disj-distr-uni-com, uni-com,
uni-ac3-trueprovedall subs proved uni-acall-true, disj-com-rw, uni-com,
uni-ac2-trueprovedall subs proved uni-acall-true, uni-com,
subset-union31provedall subs proved subset-union, disj-distr-uni,
uni-acall-trueprovedall subs proved uni-ac1-true, uni-ass, disj-com-rw, disj-distr-uni-com, uni-com,
subset-union2provedall subs proved subset-union, uni-com,
uni-ac1-trueprovedall subs proved uni-com-true, uni-inj, disj-com-rw, disj-distr-uni,
subset-unionprovedall subs proved disj-com-rw, uni-inj, subset-uni,
uni-ass-trueprovedall subs proved uni-ass,
union-diff1provedall subs proved uni-emp-l, disj-diff-id2, same-diff-empty, union-diff-distr,
union-diff2provedall subs proved uni-emp, same-diff-empty, disj-diff-id1, union-diff-distr,
union-diff-distrprovedall subs proved disj-r, disj-l, disj-diffb, at-uni, in-uni, diff-at, diff-in,
uni-emp-lprovedall subs proved uni-emp, disj-emp-r, uni-com,
uni-com-trueprovedall subs proved uni-com,
subset-uniprovedall subs proved disj-r, subset, subset-at, diff-at, disj-l, at-uni, subset-in, diff-in, in-uni, uni-com, disj-diff-same,
uni-assprovedall subs proved at-uni, disj-distr-uni, disj-com-rw, disj-distr-uni-com, in-uni,
uni-inj2provedall subs proved uni-inj, uni-com,
union-add-singleton-leftprovedall subs proved union-add-singleton-right, disj-emp-r, disj-write, uni-com,
write-leftprovedall subs proved uni-write, disj-com-rw, disj-r, disj, uni-com,
disj-distr-uni-comprovedall subs proved disj-distr-uni, disj-com,
disj-diffbprovedall subs proved disj-diffr, disj-diffl,
uni-comprovedall subs proved disj-l, at-uni, disj-com-rw, in-uni,
uni-injprovedall subs proved disj-r, disj-l, at-uni, in-uni,
union-subsetprovedall subs proved disj-r, at-uni, in-uni, subset,
union-left-singleton-atprovedall subs proved disj-singleton-write, in-uni, at-uni,
union-left-singletonprovedall subs proved at-uni, disj-singleton-write, in-uni,
del-uniprovedall subs proved disj-r, disj-rem, at-uni, in-uni,
disj-diff-id2provedall subs proved disj-diff-id1, disj-com,
disj-diffrprovedall subs proved disj-diffl, disj-com-rw, disj-com,
disj-distr-uniprovedall subs proved disj-l, in-uni, disj,
disj-union-diffprovedall subs proved in-uni, subset, diff-in, disj,
at-uniprovedall subs proved disj-r, disj-l, disj-write, uni-alloc, uni-write, disj-alloc, disj-emp-r, uni-emp, in-uni,
exin-uniprovedall subs proved union-add-singleton-right,
size-uniprovedall subs proved disj-write, size-alloc, size-write, in-uni, uni-alloc, uni-write, disj-alloc, size-emp, uni-emp,
union-add-singleton-rightprovedall subs proved uni-emp, uni-alloc, disj-emp-r, disj-r, disj, uni-write,
disj-difflprovedall subs proved disj-r, diff-in, disj,
disj-comprovedall subs proved disj-com-rw,
in-uniprovedall subs proved size-alloc, size-write, disj-write, uni-alloc, uni-write, disj-alloc, uni-emp,
delswrprovedall subs proved diffs-sw, diffs-ins,
diff-sizeprovedall subs proved in-diffs, diffs-sw, diffs-ins, diffs-emp,
disj-remprovedall subs proved disj-l, disj,
same-diff-emptyprovedall subs proved diff-in,
disj-diff-sameprovedall subs proved diff-in, disj,
diffs-swprovedall subs proved at-diffs, in-diffs,
disj-diff-id1provedall subs proved diff-in, diff-at, disj-l,
disj-allocprovedall subs proved disj-l, disj,
disj-writeprovedall subs proved disj-l, disj,
disj-rprovedall subs proved disj-l,
disj-com-rwprovedall subs proved disj-l, disj,
disj-diffprovedall subs proved diff-in, disj,
subset-at-sucprovedall subs proved subset-at,
subset-diffemptyprovedall subs proved subset-in, diff-in,
subset-empprovedall subs proved subset, emp-subset,
sw-del-add-newprovedall subs proved at-diffs, in-diffs,
subset-at-antprovedall subs proved subset-at,
diffs-twiceprovedall subs proved in-diffs, at-diffs,
disj-singleton-writeprovedall subs proved disj,
in-diffsprovedall subs proved diffs-ins, diffs-emp,
at-diffsprovedall subs proved diffs-ins, diffs-emp,
emp-subsetprovedall subs proved subset,
subset-inprovedall subs proved subset,
subset-atprovedall subs proved subset,
disj-emp-rprovedall subs proved disj,
diff-inprovedall subs proved diff-alloc, diff-write, diff-emp,
diff-atprovedall subs proved diff-alloc, diff-write, diff-emp,
disj-lprovedall subs proved disj,
subset-transprovedall subs proved subset,
add-subsetprovedall subs proved subset,
subset-reflprovedall subs proved subset,
write-rightprovedall subs proved uni-write,
subset-addnewprovedall subs proved subset,
sw-delswrprovedall subs proved diffs-ins, diffs-emp,
disj-emp-lprovedall subs proved disj,
size-empaxiom
diffs-empaxiom
diffs-insaxiom
uni-writeaxiom
uni-allocaxiom
size-writeaxiom
size-allocaxiom
disjaxiom
uni-empaxiom
diff-empaxiom
diff-writeaxiom
diff-allocaxiom
subsetaxiom