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

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:
sepprovedall subs proved uni, at-unir, at-unil, at-mk, in-mk, in-uni, disj, mk-exists, apply,
split-uniprovedall subs proved disj, uni, apply,
uniprovedall subs proved at-unir, at-unil, at-mk, in-mk, in-uni,
at-unilprovedall subs proved at-mk, in-mk, disj, in-uni,
at-unirprovedall subs proved at-mk, in-mk, disj, in-uni,
mk-extprovedall subs proved mk-exists, apply,
mk-existsprovedall subs proved at-mk, in-mk, emp,
in-uniprovedall subs proved in-mk, disj,
at-rw0provedall subs proved at-rw, apply,
map-putprovedall subs proved in-mk, write, apply,
mapex-in0provedall subs proved mapex-in, apply,
map-delprovedall subs proved at-mk, in-mk, del, apply,
mapex-putprovedall subs proved at-mk, in-mk, write, apply,
map-putrevprovedall subs proved in-mk, apply, write,
mapex-delprovedall subs proved del, apply,
map-in0provedall subs proved map-in, apply,
map-inprovedall subs proved at-mk, in-mk, apply,
empprovedall subs proved in-mk,
delprovedall subs proved at-mk, in-mk,
mapex-inprovedall subs proved at-mk, in-mk, apply,
writeprovedall subs proved at-mk, in-mk,
at-rwprovedall subs proved at-mk, in-mk, apply,
disjprovedall subs proved in-mk,
prop-sepprovedall subs proved apply,
ex2-shiftprovedall subs proved apply,
true-empprovedall subs proved apply,
propprovedall subs proved apply,
mapex-newprovedall subs proved at-mk, in-mk, apply,
prop-trueprovedall subs proved apply,
prop-empprovedall subs proved apply,
true-elimprovedall subs proved apply,
ex3-shiftprovedall subs proved apply,
mapex-elimprovedall subs proved apply,
prop-falseprovedall subs proved apply,
ex1-shiftprovedall subs proved apply,
in-mkaxiom
at-mkaxiom
applyaxiom