[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 refmap-separation

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:
exec-assign-wpprovedall subs proved free-unknown, eq,
free-unknownprovedall subs proved eq, free-notin,
assigned-known-getothermapletprovedall subs proved assigned-known-getother, eq,
free-knownprovedall subs proved eq, free-notin,
free-notinprovedall subs proved eq,
assigned-known-getotherprovedall subs proved eq,
eq-cong-injlprovedall subs proved eq,
assign-unknown-weakprovedall subs proved eq,
in-assignprovedall subs proved eq,
eq-cong-injrprovedall subs proved eq,
collapse-assignsprovedall subs proved eq,
get-assignprovedall subs proved eq,
in-addprovedall subs proved eq,
assign-known-weakprovedall subs proved eq,
eq-atprovedall subs proved eq,
assign-new-otherprovedall subs proved eq,
in-removeprovedall subs proved eq,
assign-wpprovedall subs proved eq,
eq-otherprovedall subs proved eq,
assigned-known-getother2provedall subs proved eq,
eq-sameprovedall subs proved eq,
eqaxiom