[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 build-base

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:
unique-prefix-nilprovedall subs proved unique-prefix,
unique-prefixprovedall subs proved min-le, depths-min, depths-nonnil, depths-node, first-in, depths-leaf,
in-depths-gtprovedall subs proved depths-min, min-le,
depths-oneprovedall subs proved depths-size-one, depths-leaf,
first-inprovedall subs proved depths-nonnil,
depths-minprovedall subs proved min-concat, depths-nonnil, depths-node, min-one, depths-leaf,
depths-size-oneprovedall subs proved depths-nonnil, depths-node, depths-leaf,
depths-maxprovedall subs proved max-concat, depths-nonnil, depths-node, max-one, depths-leaf,
max-gt-recprovedall subs proved max-ge,
min-le-maxprovedall subs proved max-in, min-le,
max-concatprovedall subs proved max-rec, max-one,
min-concatprovedall subs proved min-rec, min-one,
max-geprovedall subs proved max-rec, max-one,
max-inprovedall subs proved max-rec, max-one,
min-leprovedall subs proved min-rec, min-one,
depths-nonnilprovedall subs proved depths-node, depths-leaf,
min-inprovedall subs proved min-rec, min-one,
min-recaxiom
max-recaxiom
min-oneaxiom
depths-leafaxiom
max-oneaxiom
depths-nodeaxiom