[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-last

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:
nodups-butlastnprovedall subs proved lb, blastN-all-01, butlast-one, bapp, butlastN-rec, blastN-rec-01, butlastN-base,
blastN-all-01provedall subs proved blastN-all,
b-02provedall subs proved butlast-one, bc,
consmklist-lastprovedall subs proved last-one, mk-zero, mk-last-01-01,
l-03provedall subs proved l-02,
l-04provedall subs proved l-02,
lastcons-inprovedall subs proved lin-01, l-02, last-one,
linprovedall subs proved lin-01, lapp,
lin-02provedall subs proved lin-01,
prefix-equalityprovedall subs proved prefix-eq, prefix-self,
prefix-last-simpprovedall subs proved prefix-app, prefix-attach,
prefix-attachprovedall subs proved prefix-app-06, prefix-self, prefix-split-stronger, prefix-one-01,
prefix-eqprovedall subs proved prefix-app-01, prefix, prefix-self, prefix-trans,
lin-01provedall subs proved l-in, last-one,
l-02provedall subs proved lapp,
mk-last-01-01provedall subs proved mk-last-01, mk-empty, lapp,
blastN-allprovedall subs proved blastN-len,
bcprovedall subs proved bapp,
blastn-len-0provedall subs proved blastN-len,
lapp-02provedall subs proved lapp,
mklist-rmdupprovedall subs proved mk-elem, mklist-rmdup-01,
prefix-app-transprovedall subs proved prefix, prefix-trans,
prefix-exprovedall subs proved prefix-app-06, prefix-rec-01, prefix-empty, prefix-nil,
prefix-oneprovedall subs proved prefix-rec, prefix-app-05,
prefix-splitprovedall subs proved prefix-app-06, prefix-split-stronger,
prefix-recprovedall subs proved prefix-rec-03,
prefix-rec-01provedall subs proved prefix-rec-03, prefix-empty,
prefix-split-strongerprovedall subs proved prefix-rec-03, prefix-empty, prefix-nil,
prefix-transprovedall subs proved prefix-rec-03, prefix-nil, prefix-empty,
blastN-rec-01provedall subs proved butlast-def, butlastN-rec, blastN-rec, butlastN-base,
mklist-rmdup-01provedall subs proved mk-in, mk-last, mk-last-02, mklist-one,
mk-last-01provedall subs proved last-def, mk-last-02,
l-inprovedall subs proved lapp-01, last-one,
lappprovedall subs proved lapp-01,
blastN-lenprovedall subs proved blastN-rec, butlastN-base,
bappprovedall subs proved bin,
b-01provedall subs proved l-06, blapp,
blprovedall subs proved lapp-01, bin, last-one, butlast-one,
blastN-mklistprovedall subs proved butlast-def, mk-last-02, butlastN-rec, butlastN-base, mk-zero,
blastn-app-1provedall subs proved butlastN-base, blastN-rec,
lapp-03provedall subs proved lapp-01,
last-sizeoneprovedall subs proved last-one, lapp-01,
lthreeprovedall subs proved lapp-01,
mk-butlastprovedall subs proved butlast-def, mk-last-02,
mk-butlast-01provedall subs proved mk-inj-01, butlast-def, mk-last-02,
mk-prefixprovedall subs proved mk-empty, mklist-split-intro, prefix,
postfix-recprovedall subs proved postfix-app-06, last-elim,
rev-disjointprovedall subs proved rev-disjoint-01, rev-one, rev-app, rev-e,
rev-mklistprovedall subs proved mk-last, rev-r, mk-last-02, mk-zero, rev-e,
splitlasteqprovedall subs proved blapp, last-def, butlast-def,
splitlasteq-01provedall subs proved blapp, last-def, butlast-def,
rev-disjoint-01provedall subs proved rev-in,
prefix-rec-03provedall subs proved prefix, prefix-rec-02,
postfix-app-06provedall subs proved postfix, postfix-same,
mklist-split-introprovedall subs proved mk-plus,
mk-last-02provedall subs proved mklist-one, mk-plus,
blastN-recprovedall subs proved butlast-def, butlastN-rec,
lapp-01provedall subs proved last-def, last-elim,
binprovedall subs proved butlast-rec, butlast-one, butlast-def,
blappprovedall subs proved last-elim, butlast-last,
blast-headprovedall subs proved last-elim, bin-01,
butlast-eqprovedall subs proved last-elim, butlast-last,
butlast-last-01provedall subs proved butlast-last,
butlast-lenprovedall subs proved lb,
lapp-04provedall subs proved last-def,
lapp-05provedall subs proved last-def,
lastprovedall subs proved butlast-last,
last-01provedall subs proved last-def,
lb-01provedall subs proved lb,
map-lastprovedall subs proved last-def, last-elim,
mk-injprovedall subs proved mk-in, mk-inj-01, mk-elem, mk-rec, mk-empty, mk-zero,
mk-prefix-appprovedall subs proved mk-plus, prefix,
mklist-appendprovedall subs proved mk-plus,
mklist-lastprovedall subs proved mk-last, mklist-one, mk-plus,
prefix-butlast-appendprovedall subs proved prefix-app-06, prefix-one-01, last-elim, prefix-self, butlast-last,
prefix-same-01provedall subs proved prefix-same,
rev-dupsprovedall subs proved rev-in, rev-r, rev-e,
rev-rewriteprovedall subs proved rev-rev-identity,
rev-tailprovedall subs proved rev-one, rev-app, rev-in, rev-empty,
revert-equalprovedall subs proved rev-rev-identity,
rev-emptyprovedall subs proved rev-one, rev-app, rev-e,
rev-rev-identityprovedall subs proved rev-one, rev-app, rev-e,
rev-inprovedall subs proved rev-one, rev-app, rev-e,
prefix-sameprovedall subs proved prefix-app-06, prefix,
prefix-rec-02provedall subs proved prefix-app-06, prefix,
prefix-appprovedall subs proved prefix-app-05, prefix,
prefix-app-01provedall subs proved prefix-app-06, prefix-empty, prefix-self,
postfix-sameprovedall subs proved postfix-app-01, postfix-app-02, postfix,
mk-plusprovedall subs proved mk-last, mk-succ, mk-zero,
mk-inj-01provedall subs proved mk-in, mk-rec, mk-empty, mk-zero,
last-defprovedall subs proved last-elim,
lbprovedall subs proved last-elim,
bin-01provedall subs proved last-elim,
butlast-lastprovedall subs proved last-elim,
butlast-defprovedall subs proved last-elim,
bin-02provedall subs proved last-elim,
bnotemptyprovedall subs proved last-elim,
last-exprovedall subs proved last-elim,
mk-headprovedall subs proved mk-rec, mk-elem, mk-empty,
mk-head-01provedall subs proved mk-elem, mk-empty,
mk-oneprovedall subs proved mk-empty, mk-succ, mklist-one,
mk-one-01provedall subs proved mk-empty, mk-rec, mk-zero, mklist-one,
mk-tailprovedall subs proved mk-rec, mk-empty,
mk-tail-01provedall subs proved mk-rec, mk-in, mk-elem, mk-empty,
mk-twoprovedall subs proved mk-rec,
mk-two-01provedall subs proved mklist-one, mk-succ,
postfix-empty-03provedall subs proved postfix-empty, postfix,
postfix-inprovedall subs proved postfix-in-01,
postfix-in-02provedall subs proved postfix-in-01,
postfix-one-lessprovedall subs proved postfix-app,
postfix-splitprovedall subs proved postfix-app-01, postfix-split-stronger, postfix,
prefix-app-02provedall subs proved prefix-longer-01, prefix-self,
prefix-app-03provedall subs proved prefix-longer-01, prefix-self,
prefix-app-size-eqprovedall subs proved prefix, prefix-app-05,
prefix-butlastprovedall subs proved prefix-app-04, last-elim,
prefix-comparableprovedall subs proved prefix, two-prefixes,
prefix-empty-03provedall subs proved prefix-empty,
prefix-introprovedall subs proved prefix-app-05,
prefix-notinprovedall subs proved prefix-in-02,
prefix-of-twoprovedall subs proved prefix-empty, prefix,
prefix-size-eqprovedall subs proved prefix, prefix-self,
revert-lastprovedall subs proved rev-one, rev-app,
rev-appprovedall subs proved rev-r, rev-e,
rev-oneprovedall subs proved rev-e, rev-r,
prefix-in-02provedall subs proved prefix,
prefix-nilprovedall subs proved prefix,
two-prefixesprovedall subs proved prefix,
prefix-app-04provedall subs proved prefix,
prefix-one-01provedall subs proved prefix,
prefix-longer-01provedall subs proved prefix,
prefix-selfprovedall subs proved prefix,
prefix-emptyprovedall subs proved prefix,
prefix-app-06provedall subs proved prefix,
prefix-app-05provedall subs proved prefix,
postfix-split-strongerprovedall subs proved postfix,
postfix-app-02provedall subs proved postfix,
postfix-app-01provedall subs proved postfix,
postfix-appprovedall subs proved postfix,
postfix-in-01provedall subs proved postfix,
postfix-emptyprovedall subs proved postfix,
mk-lastprovedall subs proved mk-succ, mk-zero,
mklist-oneprovedall subs proved mk-zero, mk-succ,
mk-inprovedall subs proved mk-succ, mk-zero,
mk-emptyprovedall subs proved mk-succ, mk-zero,
mk-elemprovedall subs proved mk-succ, mk-zero,
mk-recprovedall subs proved mk-succ,
last-elimprovedall subs proved butlast-rec, last-rec, butlast-one, last-one,
l-06provedall subs proved last-one,
l-01provedall subs proved last-one,
le-leq-one-empty-or-head-equal-lastprovedall subs proved last-one,
mk-lenprovedall subs proved mk-succ, mk-zero,
postfix-in-03provedall subs proved postfix,
postfix-is-lessOrEqualprovedall subs proved postfix,
postfix-lengthprovedall subs proved postfix,
postfix-moreprovedall subs proved postfix,
postfix-more-01provedall subs proved postfix,
postfix-oneprovedall subs proved postfix,
postfix-rec-rightprovedall subs proved postfix,
postfix-reflexivityprovedall subs proved postfix,
postfix-tailprovedall subs proved postfix,
postfix-tail-01provedall subs proved postfix,
postfix-transprovedall subs proved postfix,
prefix-inprovedall subs proved prefix,
prefix-in-01provedall subs proved prefix,
prefix-in-03provedall subs proved prefix,
prefix-longerprovedall subs proved prefix,
prefix-moreprovedall subs proved prefix,
rev-lengthprovedall subs proved rev-r, rev-e,
rev-eaxiom
rev-raxiom
postfixaxiom
prefixaxiom
mk-succaxiom
last-recaxiom
mk-zeroaxiom
butlastN-recaxiom
butlastN-baseaxiom
last-oneaxiom
butlast-recaxiom
butlast-oneaxiom