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

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:
unwind-SD-theoremprovedall subs proved unwind-BSD-theorem,
unwind-BSD-theoremprovedall subs proved lrf-def, lemma-5-4-2,
unwind-BSRA-theoremprovedall subs proved xlrf-intro, xlrf-property,
xlrf-propertyprovedall subs proved osc-intro, xlrf-intro, xosc-is-osc,
lemma-5-4-2provedall subs proved osc-help,
osc-helpprovedall subs proved osc-def,
osc-introprovedall subs proved osc-def,
xlrf-introprovedall subs proved xlrf-def,
xosc-is-oscprovedall subs proved xosc-def, osc-def,
lrf-introprovedall subs proved lrf-def,
isEqRel-transitiveprovedall subs proved isEqRel-def,
isEqRel-symmetricprovedall subs proved isEqRel-def,
isEqRel-reflexiveprovedall subs proved isEqRel-def,
xosc-defaxiom
xlrf-defaxiom
osc-defaxiom
lrf-defaxiom
isEqRel-defaxiom