[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 oarray-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-write-otherprovedall subs proved less-eq-elem, sorted,
sorted-shift-oneprovedall subs proved less-eq-elem, sorted,
sorted-mixupprovedall subs proved less-eq-elem, sorted,
sorted-mergeprovedall subs proved less-eq-elem, sorted,
sorted-lower-higher-boundprovedall subs proved less-eq-elem, sorted,
sorted-insert-mergeprovedall subs proved sorted, less-eq-elem,
sorted-inc-rightprovedall subs proved sorted, less-eq-elem,
sorted-inc-leftprovedall subs proved sorted, less-eq-elem,
sorted-higher-lower-boundprovedall subs proved less-eq-elem, sorted,
sorted-emtpyprovedall subs proved sorted,
sorted-2provedall subs proved sorted, less-eq-elem,
sorted-1-moreprovedall subs proved less-eq-elem, sorted,
sorted-1provedall subs proved sorted,
sorted-0-or-1provedall subs proved less-eq-elem, sorted,
sortedaxiom
less-eq-elemaxiom