[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 list-prefixn

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:
slice-range0provedall subs proved prefixn-0, dropn, slice,
prefixn-0provedall subs proved prefixn,
prefixn-split-sublistprovedall subs proved prefixn,
prefixn-split-dropnprovedall subs proved dropn, prefixn,
prefixn-size-prefixnprovedall subs proved prefixn,
prefixn-size-eqprovedall subs proved prefixn,
prefixn-single-1provedall subs proved prefixn,
prefixn-prefixnprovedall subs proved prefixn,
prefixn-notinprovedall subs proved prefixn,
prefixn-nodupsprovedall subs proved prefixn,
prefixn-neq-empty-plusoneprovedall subs proved prefixn,
prefixn-len-nprovedall subs proved prefixn,
prefixn-len-le-nprovedall subs proved prefixn,
prefixn-le-sizeprovedall subs proved prefixn,
prefixn-inprovedall subs proved prefixn,
prefixn-fullnprovedall subs proved prefixn,
prefixn-full-eqprovedall subs proved prefixn,
prefixn-fullprovedall subs proved prefixn,
prefixn-eq-appendprovedall subs proved prefixn,
prefixn-emptyprovedall subs proved prefixn,
prefixn-butlastprovedall subs proved prefixn,
prefixn-append-sliceprovedall subs proved dropn, slice, prefixn,
prefixn-append-prefixprovedall subs proved prefixn,
prefixn-append-leftprovedall subs proved prefixn,
prefix-prefixn-sameprovedall subs proved prefixn,
prefix-prefixn-not-shorterprovedall subs proved prefixn,
prefix-prefixn-exactprovedall subs proved prefixn,
in-prefixn-sameposprovedall subs proved prefixn,
in-prefixn-pos-smaller0provedall subs proved prefixn,
in-prefixn-pos-smallerprovedall subs proved prefixn,
in-prefixn-in-shorter-prefixprovedall subs proved prefixn,
in-prefixn-at-smallerprovedall subs proved prefixn,
dropn-firstprovedall subs proved dropn,
dropn-emptyprovedall subs proved dropn,
dropn-0provedall subs proved dropn,
sliceaxiom
prefixnaxiom
dropnaxiom