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: |
|---|
| remnone-cntequal | proved | all subs proved
| rem-member1,
cnt-is-zero,
cntinf-fin-weak,
remfin-fin2,
cnt-appendfromto,
remfin-append,
cntinf-tocntsurj,
rem-cntequal-fin,
|
| rem-cntequal-fin | proved | all subs proved
| cntfin-notinf,
rem-cntleq,
rem-rec-rev,
cnt-rec-gen,
cnt-zero,
rem-base,
|
| cntinf-tocntsurj | proved | all subs proved
| mon-cntto,
cntto-notinf,
cnt-is-zero,
cnt-appendfromto,
cnt-rec-end,
cnt-zero,
filter-infsize,
count-def,
|
| mon-cnttoinf | proved | all subs proved
| mon-cntto,
|
| rem-cntleq | proved | all subs proved
| rem-member1,
cnt-is-zero,
remfin-fin2,
cnt-appendfromto,
remfin-append,
cntinf-fin-weak,
cnt-rec-gen,
rem-rec-rev,
rem-base,
cnt-zero,
|
| mon-cntto | proved | all subs proved
| cnt-appendfromto,
|
| rem-reminv-cnt-add | proved | all subs proved
| rem-member1,
cnt-is-zero,
remfin-fin2,
cnt-appendfromto,
remfin-append,
cntinf-fin-weak,
cntrem-is-inf,
cnt-inf,
cnt-rec-gen,
rem-rec-rev,
cnt-zero,
rem-base,
|
| mon-filtertoinf | proved | all subs proved
| mon-filterto,
|
| lastocfin-cnteqcntto | proved | all subs proved
| cnt-is-succ,
cnt-is-zero,
cnt-inf,
cntto-notinf,
lastoc-fin,
|
| cntrem-is-inf | proved | all subs proved
| reminf-infsize,
rem-member2,
remfin-append,
rem-member1,
rem-shortens,
reminf-infsize-strong,
remfin-fin2,
cnt-inf,
|
| mon-filterto | proved | all subs proved
| to-is-prefix,
mon-filterprefix,
|
| cnt-is-succ | proved | all subs proved
| cntinf-fin-succ,
cnt-one,
cnt-is-zero,
cnt-rec-gen,
cnt-zero,
|
| cnt-appendfromto | proved | all subs proved
| filter-appendfromto,
count-def,
|
| rem-reminv-size-add | proved | all subs proved
| reminf-finsize,
rem-rec-rev,
rem-base,
|
| mon-cntprefix | proved | all subs proved
| prefix-notsmallersize,
mon-filterprefix,
count-def,
|
| reminf-finsize | proved | all subs proved
| rem-rec,
lim-infsize,
remfin-fin2,
lim-finsize,
rem-inf,
mon-remfun,
reminf-infsize,
|
| cntinf-fin-weak | proved | all subs proved
| cntinf-fin-succ,
cntfin-rec-end,
cnt-zero,
cntinf-fin-zero,
|
| mon-filterprefix | proved | all subs proved
| prefix-refl,
prefix-append,
filterfin-append,
prefix-def,
|
| rem-member1 | proved | all subs proved
| prefix-def,
lim-def,
rem-inf,
reminf-infsize,
mon-remfun,
rem-member1-fin,
|
| remfin-append | proved | all subs proved
| rem-rec-rev,
rem-base,
|
| rem-member2 | proved | all subs proved
| rem-rec-rev,
rem-member2-fin,
|
| cnt-is-zero | proved | all subs proved
| filterfin-rec-end,
prefix-empty2,
prefix-empty1,
mon-filterfun,
lim-def,
filter-inf,
count-def,
cnt-rec-gen,
cnt-zero,
|
| filter-appendfromto | proved | all subs proved
| filterfin-append,
|
| cntnotinf-lastocinf | proved | all subs proved
| lastoc-rw-inf,
lastoc-inf-ant,
cnt-inf,
|
| cntinf-lastocinf | proved | all subs proved
| lastoc-rw-inf,
cnt-inf,
|
| cntfin-eqlen | proved | all subs proved
| cnt-rec-gen,
cnt-leq,
cnt-zero,
|
| cntfin-append | proved | all subs proved
| filterfin-append,
count-def,
|
| rem-rec-rev | proved | all subs proved
| lim-finsize,
mon-lem,
rem-base,
prefix-def,
lim-def,
remfin-fin2,
lim-infsize-strong,
mon-remfun,
rem-inf,
rem-rec-rev-fin,
|
| reminf-infsize-strong | proved | all subs proved
| prefix-def,
rem-rec,
mon-lem,
rem-base,
remfin-fin2,
mon-remfun,
lim-infsize-strong,
rem-inf,
|
| reminf-infsize | proved | all subs proved
| lim-finsize,
rem-rec,
remfin-fin2,
lim-infsize,
mon-remfun,
rem-inf,
|
| cnt-inf | proved | all subs proved
| filter-infsize,
count-def,
|
| filterfin-append | proved | all subs proved
| filter-rec-gen,
filter-rec,
filter-base,
|
| cnt-rec-gen | proved | all subs proved
| filter-rec-gen,
count-def,
|
| cntinf-fin-succ | proved | all subs proved
| filter-evconst,
cntfin-rec-end,
filterfin-rec-end,
filter-base,
filter-inf-finsize,
count-def,
|
| filter-rec-expand | proved | all subs proved
| filter-rec-gen,
filter-base,
|
| filter-inf-finsize-strong | proved | all subs proved
| prefix-def,
prefix-refl,
prefix-antisymm,
mon-filterfun,
lim-def,
filter-inf,
filter-inf-finsize,
|
| cntinf-infmany | proved | all subs proved
| filter-infsize,
count-def,
|
| lim-infsize-strong | proved | all subs proved
| prefix-def,
mon-lem,
lim-infsize,
|
| lim-finsize | proved | all subs proved
| prefix-def,
mon-lem,
lim-infsize,
lim-evconst,
mon-bd-or-unbound,
|
| filter-inf-finsize | proved | all subs proved
| lim-evconst,
finfilter-notinf,
prefixself-equal,
prefix-trans,
mon-lem,
filterfin-rec-end,
prefix-refl,
prefix-antisymm,
filter-lb,
mon-filterfun,
lim-def,
filter-inf,
|
| filter-rec-gen | proved | all subs proved
| prefix-append,
mon-def,
filterfin-rec-end,
lim-infsize,
finfilter-notinf,
mon-lem,
filter-base,
prefix-def,
lim-def,
lim-evconst,
mon-filterfun,
filter-inf,
filter-rec,
|
| filter-infsize | proved | all subs proved
| filterfin-rec-end,
prefix-def,
mon-lem,
mon-filterfun,
lim-infsize,
filter-inf,
finfilter-notinf,
|
| rem-member2-fin | proved | all subs proved
| remfin-fin2,
rem-rec,
|
| lim-infsize | proved | all subs proved
| prefix-refl,
prefix-antisymm,
prefix-trans,
mon-lem,
prefix-def,
lim-evconst,
lim-def,
|
| filter-lb | proved | all subs proved
| mon-filterfun,
lim-def,
filter-inf,
prefix-def,
filterfin-rec-end,
|
| cnt-rec-end | proved | all subs proved
| cntfin-rec-end,
|
| cntinf-fin-zero | proved | all subs proved
| filter-base,
filterfin-rec-end,
mon-filterfun,
prefix-empty1,
prefix-empty2,
lim-def,
filter-inf,
count-def,
|
| filter-evconst | proved | all subs proved
| filterfin-rec-end,
mon-filterfun,
lim-evconst,
filter-inf,
|
| cnt-one | proved | all subs proved
| cnt-zero,
cntfin-rec-end,
|
| remto-fin | proved | all subs proved
| remfin-fin2,
|
| rem-equal-inf | proved | all subs proved
| prefix-def,
rem-equal-fin,
mon-remfun,
lim-def,
rem-inf,
|
| getfilter-sat-p | proved | all subs proved
| prefix-def,
mon-filterfun,
lim-def,
filter-inf,
filter-rec,
filter-base,
|
| filter-ub | proved | all subs proved
| mon-filterfun,
lim-def,
filter-inf,
prefix-def,
prefix-empty1,
filter-rec,
filter-base,
|
| rem-member1-fin | proved | all subs proved
| rem-rec-rev-fin,
rem-base,
|
| rem-equal-fin | proved | all subs proved
| remfin-fin,
rem-shortens,
rem-rec,
rem-base,
|
| mon-bd-or-unbound | proved | all subs proved
| prefix-def,
mon-lem,
|
| lim-evconst | proved | all subs proved
| prefix-trans,
mon-lem,
prefix-def,
lim-def,
|
| remfin-fin2 | proved | all subs proved
| remfin-fin,
|
| cntto-notinf | proved | all subs proved
| cntfin-notinf,
|
| cntfin-rec-end | proved | all subs proved
| filterfin-rec-end,
count-def,
|
| mon-filterfun | proved | all subs proved
| prefix-append,
filterfin-rec-end,
mon-def,
|
| lim-unique | proved | all subs proved
| prefix-append,
prefix-trans,
mon-lem,
prefix-def,
|
| lim-exists | proved | all subs proved
| prefix-refl,
mon-lem,
prefix-def,
|
| lastoc-finrec-end-expand | proved | all subs proved
| lastoc-empty,
lastoc-finrec-end,
|
| rem-rec-rev-fin | proved | all subs proved
| rem-rec,
rem-base,
rem-one,
|
| mon-remfun | proved | all subs proved
| prefix-append,
rem-rec,
mon-def,
|
| remfin-fin | proved | all subs proved
| rem-shortens,
|
| to-is-prefix | proved | all subs proved
| prefix-append,
|
| lastoc-finrec-end | proved | all subs proved
| lastoc-inf-ant,
lastoc-inf,
lastoc-fin,
lastoc-rw-inf,
|
| lastoc-empty | proved | all subs proved
| lastoc-rw-inf,
|
| prefix-antisymm | proved | all subs proved
| prefixself-equal,
prefix-def,
prefix-refl,
prefix-trans,
|
| mon-lem | proved | all subs proved
| prefix-trans,
mon-def,
prefix-refl,
|
| cntfin-notinf | proved | all subs proved
| finfilter-notinf,
count-def,
|
| prefix-empty2 | proved | all subs proved
| prefix-def,
prefix-empty1,
|
| filterfin-rec-end | proved | all subs proved
| filter-rec,
filter-base,
filter-one,
|
| rem-rec-finsize | proved | all subs proved
| rem-rec-gen,
|
| lastoc-less-succsize | proved | all subs proved
| lastoc-fin,
lastoc-inf-ant,
|
| lastoc-less-size | proved | all subs proved
| lastoc-fin,
lastoc-inf-ant,
|
| rem-one | proved | all subs proved
| rem-base,
rem-rec,
|
| rem-rec-gen | proved | all subs proved
| rem-rec,
|
| prefix-notsmallersize | proved | all subs proved
| prefix-def,
|
| filter-one | proved | all subs proved
| filter-base,
filter-rec,
|
| prefix-append | proved | all subs proved
| prefix-def,
|
| prefix-refl | proved | all subs proved
| prefix-def,
|
| prefix-trans | proved | all subs proved
| prefix-def,
|
| prefixself-equal | proved | all subs proved
| prefix-def,
|
| rem-shortens | proved | all subs proved
| rem-rec,
rem-base,
|
| lastoc-inf-ant | proved | all subs proved
| lastoc-inf,
|
| lastoc-rw-inf | proved | all subs proved
| lastoc-inf,
|
| finfilter-notinf | proved | all subs proved
| filter-rec,
filter-base,
|
| cnt-leq | proved | all subs proved
| filter-rec,
filter-base,
count-def,
|
| prefix-empty1 | proved | all subs proved
| prefix-def,
|
| cnt-zero | proved | all subs proved
| filter-base,
count-def,
|
| rem-inf | axiom | | |
| rem-base | axiom | | |
| rem-rec | axiom | | |
| lastoc-fin | axiom | | |
| lastoc-inf | axiom | | |
| mon-def | axiom | | |
| prefix-def | axiom | | |
| filter-base | axiom | | |
| filter-rec | axiom | | |
| filter-inf | axiom | | |
| lim-def | axiom | | |
| count-def | axiom | | |