[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 rtc-rel

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:
rtc+-unfold-lastprovedall subs proved rtc, rtc-one, rtc-trans, rtc-refl, rtc-base, rtc-rec, rtc+,
rtc-oneprovedall subs proved rtc1, rtc,
rtc-unfoldprovedall subs proved rtc-refl, rtc-base, rtc, rtc+,
rtc1provedall subs proved rtc-base, rtc-rec,
rtc-reflprovedall subs proved rtc-base, rtc,
rtc-transprovedall subs proved rtc-rec, rtc-base, rtc,
rtc-starprovedall subs proved rtc,
rtc-lastprovedall subs proved rtc-base, rtc-rec,
rtc-is-baseprovedall subs proved rtc-base,
rtc+-unfoldprovedall subs proved rtc, rtc-rec, rtc+,
invxprovedall subs proved inv,
inv-propagateprovedall subs proved rtc-rec, rtc-base, rtc, inv,
rtc+axiom
invaxiom
rtcaxiom
rtc-baseaxiom
rtc-recaxiom