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