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: |
|---|
| postifx-split | proved | all subs proved
| postfix-app-02,
postfix-split-stronger,
|
| postfix-split-stronger | proved | all subs proved
| postfix-app-02,
lin-01,
butlast-last,
blapp-01,
lb,
bapp,
lapp,
postfix-empty-03,
postfix-empty,
postfix-rec,
|
| splitlasteq-01 | proved | all subs proved
| blapp-01,
last-def,
butlast-def,
|
| splitlasteq | proved | all subs proved
| blapp-01,
last-def,
butlast-def,
|
| b-01 | proved | all subs proved
| l,
l-06,
blapp-01,
|
| blapp-01 | proved | all subs proved
| blapp,
butlast-last,
|
| blapp | proved | all subs proved
| last-elim,
lin-01,
butlast-last,
|
| lin-02 | proved | all subs proved
| lin-01,
|
| lin | proved | all subs proved
| lin-01,
l-02,
|
| consmklist-last | proved | all subs proved
| l,
mk-zero,
mk-last-01-01,
|
| b-02 | proved | all subs proved
| b,
bc,
|
| mk-last-01-01 | proved | all subs proved
| mk-last-01,
mk-empty,
lapp,
|
| lin-01 | proved | all subs proved
| l-02,
l,
|
| bc | proved | all subs proved
| bapp,
|
| nodups-butlastn | proved | all subs proved
| lb,
blastN-all-01,
b,
bapp,
butlastN-rec,
blastN-rec-01,
butlastN-base,
|
| l-04 | proved | all subs proved
| l-02,
|
| l-03 | proved | all subs proved
| l-02,
|
| blastN-mklist | proved | all subs proved
| mk-last-02,
b,
mk-butlast,
bin,
butlastN-rec,
mk-last,
mklist-one,
mk-plus,
butlastN-base,
mk-zero,
|
| blastN-all-01 | proved | all subs proved
| blastN-all,
|
| mk-last-01 | proved | all subs proved
| mk-empty,
lapp,
l,
mk-zero,
mk-last,
mklist-one,
mk-plus,
|
| l-02 | proved | all subs proved
| lapp,
|
| mk-butlast | proved | all subs proved
| b,
mk-zero,
bin,
mk-last,
mklist-one,
mk-plus,
|
| bapp | proved | all subs proved
| bin,
|
| prefix-split | proved | all subs proved
| prefix-app-01,
postifx-app-03,
prefix-split-stronger,
|
| prefix-same-01 | proved | all subs proved
| prefix-one,
postifx-app-03,
|
| prefix-same | proved | all subs proved
| prefix-one,
postifx-app-03,
|
| prefix-equality | proved | all subs proved
| prefix-self,
prefix-eq,
|
| prefix-attach | proved | all subs proved
| prefix-app-01,
prefix-split-stronger,
prefix-one-01,
postifx-app-03,
|
| mklist-rmdup | proved | all subs proved
| mk-elem,
mklist-rmdup-01,
|
| mk-inj | proved | all subs proved
| mk-inj-01,
mk-rec,
mk-in,
mk-elem,
mk-last,
mklist-one,
mk-plus,
|
| lapp-02 | proved | all subs proved
| lapp,
|
| l-in | proved | all subs proved
| l-05,
l,
|
| prefix-one | proved | all subs proved
| prefix-rec,
prefix-app-05,
|
| prefix-eq | proved | all subs proved
| prefix-app-01,
prefix,
prefix-self,
prefix-trans,
|
| prefix-split-stronger | proved | all subs proved
| prefix-app-01,
postifx-app-03,
prefix-rec-03,
prefix-empty,
prefix-nil,
|
| mklist-rmdup-01 | proved | all subs proved
| mk-in,
mk-last,
mk-last-02,
mklist-one,
|
| mk-inj-01 | proved | all subs proved
| mk-in,
mk-rec,
mk-empty,
mk-zero,
|
| l-05 | proved | all subs proved
| lapp-01,
|
| lapp | proved | all subs proved
| lapp-01,
|
| blastN-all | proved | all subs proved
| blastN-len,
|
| bin | proved | all subs proved
| btwo,
b,
butlast-def,
|
| rev-mklist | proved | all subs proved
| rev-r,
mk-last,
mk-last-02,
rev-e,
mk-zero,
|
| prefix-more | proved | all subs proved
| prefix-app-01,
|
| prefix-longer | proved | all subs proved
| prefix-app-01,
|
| prefix-ex | proved | all subs proved
| prefix-app-01,
prefix-rec-02,
prefix-rec-01,
prefix-empty,
prefix-nil,
postifx-app-03,
|
| mk-one | proved | all subs proved
| mk-one-01,
mk-empty,
mklist-one,
|
| mk-butlast-01 | proved | all subs proved
| btwo,
b,
mk-zero,
mk-last,
mklist-one,
mk-plus,
|
| lthree | proved | all subs proved
| lapp-01,
|
| lb-01 | proved | all subs proved
| lb,
|
| last-one | proved | all subs proved
| l,
lapp-01,
|
| lapp-03 | proved | all subs proved
| lapp-01,
|
| butlast-len | proved | all subs proved
| lb,
|
| blastn-len-0 | proved | all subs proved
| blastN-len,
|
| blast-first | proved | all subs proved
| last-elim,
bin-01,
|
| prefix-rec | proved | all subs proved
| prefix-rec-03,
|
| prefix-rec-01 | proved | all subs proved
| prefix-rec-03,
prefix-empty,
|
| prefix-trans | proved | all subs proved
| prefix-rec-03,
prefix-nil,
prefix-empty,
|
| prefix-app-01 | proved | all subs proved
| prefix-rec-03,
prefix-empty,
prefix-self,
|
| postfix-rec | proved | all subs proved
| postfix-app-06,
postfix-same,
last-elim,
|
| blastN-rec-01 | proved | all subs proved
| butlast-def,
butlastN-rec,
blastN-rec,
butlastN-base,
|
| mk-one-01 | proved | all subs proved
| mk-empty,
mk-last,
mk-plus,
mk-zero,
mklist-one,
|
| mk-rec | proved | all subs proved
| mk-last,
mklist-one,
mk-plus,
|
| lapp-01 | proved | all subs proved
| last-def,
last-elim,
|
| lb | proved | all subs proved
| last-elim,
|
| mk-last-02 | proved | all subs proved
| mklist-one,
mk-plus,
mk-last,
|
| blastN-len | proved | all subs proved
| blastN-rec,
butlastN-base,
|
| bin-01 | proved | all subs proved
| last-elim,
|
| btwo | proved | all subs proved
| butlast-def,
last-elim,
|
| prefix-butlast-append | proved | all subs proved
| prefix-one-01,
postifx-app-03,
last-elim,
prefix-self,
butlast-last,
|
| prefix-butlast | proved | all subs proved
| prefix-app-04,
last-elim,
|
| postfix-rest-01 | proved | all subs proved
| postfix-one-less,
|
| mklist-split-intro | proved | all subs proved
| mk-plus,
|
| mklist-last | proved | all subs proved
| mklist-one,
mk-plus,
mk-last,
|
| mklist-append | proved | all subs proved
| mk-plus,
|
| mk-two | proved | all subs proved
| mk-last,
mklist-one,
mk-two-01,
mk-zero,
mk-plus,
|
| mk-rest-01 | proved | all subs proved
| mk-last,
mklist-one,
mk-plus,
|
| mk-rest | proved | all subs proved
| mk-last,
mklist-one,
mk-plus,
|
| last-ex | proved | all subs proved
| last-elim,
|
| butlast-eq | proved | all subs proved
| last-elim,
butlast-last,
|
| bnotempty | proved | all subs proved
| last-elim,
|
| blastn-app-1 | proved | all subs proved
| butlastN-base,
blastN-rec,
|
| bin-02 | proved | all subs proved
| last-elim,
|
| prefix-rec-03 | proved | all subs proved
| prefix-rec-02,
prefix,
|
| postfix-one-less | proved | all subs proved
| postfix-app,
|
| postfix-app-06 | proved | all subs proved
| postfix-same,
postfix,
|
| mk-two-01 | proved | all subs proved
| mklist-one,
mk-succ,
|
| mk-plus | proved | all subs proved
| mk-last,
mk-succ,
mk-zero,
|
| blastN-rec | proved | all subs proved
| butlast-def,
butlastN-rec,
|
| last-elim | proved | all subs proved
| butlast-def,
last-def,
butlast-last,
|
| l-06 | proved | all subs proved
| l,
|
| revert-equal | proved | all subs proved
| rev-rev-identity,
|
| rev-rewrite | proved | all subs proved
| rev-rev-identity,
|
| rev-disjoint | proved | all subs proved
| rev-disjoint-01,
rev-r,
rev-e,
|
| postfix-is-lessOrEqual | proved | all subs proved
| postfix-rec-right,
postfix-empty,
postfix-empty-03,
|
| postfix-in-02 | proved | all subs proved
| postfix-in-01,
|
| mk-first-01 | proved | all subs proved
| mk-elem,
mk-empty,
|
| mk-first | proved | all subs proved
| mk-elem,
mk-empty,
|
| le-leq-one-empty-or-first-equal-last | proved | all subs proved
| l,
|
| l-01 | proved | all subs proved
| l,
|
| rev-rev-identity | proved | all subs proved
| rev-one,
rev-app,
rev-r,
rev-e,
|
| rev-disjoint-01 | proved | all subs proved
| rev-in,
|
| prefix-rec-02 | proved | all subs proved
| postifx-app-03,
|
| postfix-app | proved | all subs proved
| postfix-app-01,
postfix,
|
| postfix-rec-right | proved | all subs proved
| postfix-one,
postfix-app-02,
postfix,
|
| postfix-in-01 | proved | all subs proved
| postfix-in,
|
| postfix-same | proved | all subs proved
| postfix-app-02,
|
| mk-in | proved | all subs proved
| mk-succ,
mk-zero,
|
| mk-empty | proved | all subs proved
| mk-succ,
mk-zero,
|
| mklist-one | proved | all subs proved
| mk-zero,
mk-succ,
|
| mk-last | proved | all subs proved
| mk-succ,
mk-zero,
|
| butlast-def | proved | all subs proved
| last-def,
last-02,
|
| l | proved | all subs proved
| b,
last-02,
|
| revert-last | proved | all subs proved
| rev-one,
rev-app,
|
| rev-rest | proved | all subs proved
| rev-r,
rev-in,
rev-empty,
|
| rev-dups | proved | all subs proved
| rev-in,
rev-r,
rev-e,
|
| prefix-size-eq | proved | all subs proved
| prefix,
prefix-self,
|
| prefix-notin | proved | all subs proved
| prefix-in-02,
|
| prefix-intro | proved | all subs proved
| prefix-app-05,
|
| prefix-empty-03 | proved | all subs proved
| prefix-empty,
|
| prefix-app-size-eq | proved | all subs proved
| prefix,
prefix-app-05,
|
| prefix-app-03 | proved | all subs proved
| prefix-longer-01,
prefix-self,
|
| prefix-app-02 | proved | all subs proved
| prefix-longer-01,
prefix-self,
|
| prefix-app | proved | all subs proved
| prefix-app-05,
prefix,
|
| postfix-rest | proved | all subs proved
| postfix-app-01,
|
| postfix-empty-02 | proved | all subs proved
| postfix-empty-03,
|
| postfix-empty-01 | proved | all subs proved
| postfix-empty-03,
|
| postfix-app-05 | proved | all subs proved
| postfix-app-01,
postfix-app-02,
|
| postfix-app-04 | proved | all subs proved
| postfix-app-01,
postfix-app-02,
|
| last-01 | proved | all subs proved
| last-def,
|
| lapp-05 | proved | all subs proved
| last-def,
|
| lapp-04 | proved | all subs proved
| last-def,
|
| butlast-last-01 | proved | all subs proved
| butlast-last,
|
| bl | proved | all subs proved
| butlast-last,
|
| rev-app | proved | all subs proved
| rev-r,
rev-e,
|
| rev-one | proved | all subs proved
| rev-e,
rev-r,
|
| rev-empty | proved | all subs proved
| rev-r,
rev-e,
|
| rev-in | proved | all subs proved
| rev-r,
rev-e,
|
| prefix-in-02 | proved | all subs proved
| prefix,
|
| prefix-nil | proved | all subs proved
| prefix,
|
| prefix-app-04 | proved | all subs proved
| prefix,
|
| postifx-app-03 | proved | all subs proved
| prefix,
|
| prefix-one-01 | proved | all subs proved
| prefix,
|
| prefix-longer-01 | proved | all subs proved
| prefix,
|
| prefix-self | proved | all subs proved
| prefix,
|
| prefix-empty | proved | all subs proved
| prefix,
|
| prefix-app-05 | proved | all subs proved
| prefix,
|
| postfix-one | proved | all subs proved
| postfix,
|
| postfix-empty | proved | all subs proved
| postfix,
|
| postfix-in | proved | all subs proved
| postfix,
|
| postfix-empty-03 | proved | all subs proved
| postfix,
|
| postfix-app-02 | proved | all subs proved
| postfix,
|
| postfix-app-01 | proved | all subs proved
| postfix,
|
| mk-succ | proved | all subs proved
| mk-elem,
mk-len,
|
| last-def | proved | all subs proved
| last-02,
|
| mk-zero | proved | all subs proved
| mk-len,
|
| butlast-last | proved | all subs proved
| last-02,
|
| b | proved | all subs proved
| last-02,
|
| rev-length | proved | all subs proved
| rev-r,
rev-e,
|
| prefix-in-03 | proved | all subs proved
| prefix,
|
| prefix-in-01 | proved | all subs proved
| prefix,
|
| prefix-in | proved | all subs proved
| prefix,
|
| postfix-trans | proved | all subs proved
| postfix,
|
| postfix-reflexivity | proved | all subs proved
| postfix,
|
| postfix-more-01 | proved | all subs proved
| postfix,
|
| postfix-more | proved | all subs proved
| postfix,
|
| postfix-length | proved | all subs proved
| postfix,
|
| postfix-in-03 | proved | all subs proved
| postfix,
|
| rev-e | axiom | | |
| rev-r | axiom | | |
| prefix | axiom | | |
| postfix | axiom | | |
| mk-len | axiom | | |
| mk-elem | axiom | | |
| butlastN-rec | axiom | | |
| butlastN-base | axiom | | |
| last-02 | axiom | | |