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