[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 zbranch-array-sorted

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:
sorted-eq-entry-strongprovedall subs proved sorted-eq-entry,
sorted-eq-entryprovedall subs proved sorted-all,
sorted-entry-lt-postprovedall subs proved sorted-lt-post,
sorted-branch-lt-postprovedall subs proved sorted-lt-post,
sorted-allprovedall subs proved sorted-rec, sorted-one, sorted-base, sorted-lt-h,
sorted-lt-postprovedall subs proved sorted-lt-h,
sorted-lt-preprovedall subs proved sorted-lt-h,
sorted-ltprovedall subs proved sorted-lt-h,
sorted-lt-hprovedall subs proved sorted-rec, sorted-one, sorted-base,
sorted-rec1provedall subs proved sorted-rec, sorted-base, sorted-one,
keep-sortedprovedall subs proved sorted-rec, sorted-one, sorted-base,
sorted-baseaxiom
sorted-oneaxiom
sorted-recaxiom