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: |
|---|
| toinfto-append-add | proved | all subs proved
| append-assoc,
toinf-fin,
toinftoinf-append-add,
|
| toinftoinf-append-add | proved | all subs proved
| to-append-add,
toinf-add,
toinf-fin,
size-fin,
append-assoc,
toinf-empty2,
append-cancel-l-02,
toinf-inf,
append-toinf-ls,
|
| append-from-ge-02 | proved | all subs proved
| size-inf,
append-assoc,
append-from-size-01,
size-fin,
from-zero,
append-from-gr-02,
|
| toinf-empty3 | proved | all subs proved
| to-empty3,
toinf-add,
toinf-inf,
|
| to-empty3 | proved | all subs proved
| size-succ,
to-empty2,
|
| append-toinf-ls | proved | all subs proved
| toinf-fin,
append-to-ls,
size-fin,
append-assoc,
append-cancel-l-02,
toinf-inf,
|
| toinf-empty2 | proved | all subs proved
| to-empty2,
size-empty,
toinf-inf,
to-zero,
toinf-fin,
|
| append-from-gr-02 | proved | all subs proved
| size-inf,
from-inf,
append-inf,
append-assoc,
append-from-gr-01,
size-fin,
|
| leq-symm | proved | all subs proved
| leq-symm-2,
|
| to-attach | proved | all subs proved
| append-assoc,
append-cancel-l,
append-finfin,
cons-append,
append-to-size-01,
to-succ-cons,
empty,
to-zero-l,
to-fin,
|
| toinf-empty | proved | all subs proved
| to-empty,
toinf-inf,
to-zero,
toinf-fin,
|
| append-to-addsize-01 | proved | all subs proved
| append-cancel-l,
append-assoc,
append-empty,
to-zero,
append-to-size-01,
append-to-gr-01,
|
| extensionality-to | proved | all subs proved
| size-to,
fin-to,
append-split,
to-unwind-end,
size-succ,
extensionality,
|
| append-from-ge-01 | proved | all subs proved
| from-zero,
append-assoc,
append-from-size-01,
append-from-gr-01,
|
| leq-prefix | proved | all subs proved
| finlen-tolen,
append-to-ls,
size-empty-equiv,
append-assoc,
size-append,
appendend-equal,
prefix-def,
|
| to-empty4 | proved | all subs proved
| size-empty-equiv,
to-empty2,
|
| append-to-ls | proved | all subs proved
| to-inf,
append-inf,
append-assoc,
append-to-le-01,
size-fin,
to-fin,
|
| append-from-gr-01 | proved | all subs proved
| append-assoc,
append-from-addsize-01,
|
| to-unwind-end | proved | all subs proved
| to-succ-nf,
to-inf-one,
to-zero-nf,
fun-nonempty,
one-inf,
size-inf,
sel-inf,
to-inf,
to-unwind-end-fin,
eq-stream-to-list-2-1,
sel-fin,
to-fin,
size-succ,
get-cons-succ,
append-cancel-l,
empty-append,
get-cons-zero,
to-zero,
append-empty,
cons-to-num,
append-assoc,
size-fin,
size-append,
cons-append,
to-succ-cons,
size-empty,
expand-cons,
|
| append-from-size-01 | proved | all subs proved
| from-zero,
append-from-addsize-01,
|
| append-to-gr-01 | proved | all subs proved
| append-cancel-l,
to-zero,
cons-to-num,
append-finfin,
append-assoc,
empty-append,
empty,
|
| to-empty2 | proved | all subs proved
| to-empty-inf,
to-inf,
to-empty-fin2,
size-fin,
fin-empty,
to-fin,
to-zero,
|
| to-empty | proved | all subs proved
| to-empty-inf,
to-inf,
to-empty-fin,
size-fin,
fin-empty,
to-fin,
to-zero,
|
| append-to-size-01 | proved | all subs proved
| to-all,
append-to-le-01,
|
| leq-symm-2 | proved | all subs proved
| append-assoc,
prefixself-equal,
appendend-equal,
prefix-def,
|
| toone-one | proved | all subs proved
| single-to-one,
to-fin,
append-assoc,
append-empty,
toone-cons,
|
| toinf-empty-inf | proved | all subs proved
| to-empty-inf,
fin-empty,
fun-nonempty,
toinf-inf,
empty,
to-zero-nf,
to-inf,
toinf-fin,
|
| from-infto-exchange | proved | all subs proved
| from-to-exchange,
toinf-fin,
toinf-add,
toinf-inf,
|
| from-to-exchange | proved | all subs proved
| append-assoc,
size-fin,
size-append,
cons-append,
from-succ-cons,
to-succ-cons,
size-empty,
elim-hd-tl,
from-zero,
|
| append-to-le-01 | proved | all subs proved
| append-cancel-l,
to-succ-cons-l-lem,
cons-append,
to-succ-cons,
append-finfin,
empty,
to-zero-l,
to-zero,
append-assoc,
empty-append,
|
| append-from-addsize-01 | proved | all subs proved
| from-succ-cons,
append-finfin,
append-assoc,
empty-append,
empty,
|
| prefixself-equal | proved | all subs proved
| append-assoc,
append-empty-01,
empty-append,
appendend-equal,
prefix-def,
|
| toone-cons | proved | all subs proved
| get-cons-zero,
toone-equal,
fin-empty,
append-empty-01,
append-assoc,
toone-cons-fin,
to-appfin,
|
| cons-to-num | proved | all subs proved
| append-assoc,
append-cancel-l,
cons-append,
to-succ-cons,
|
| to-empty-fin | proved | all subs proved
| elim-fromto-fin,
to-zero-l,
|
| to-empty-inf | proved | all subs proved
| elim-fromto-inf,
to-zero-nf,
|
| append-from-le-01 | proved | all subs proved
| from-succ-cons-l-lem,
from-succ-cons,
append-cancel-l,
append-finfin,
append-assoc,
empty-append,
empty,
from-zero-l,
from-zero,
|
| from-append-toinffrom | proved | all subs proved
| from-append-tofrom,
toinf-add,
toinf-fin,
append-assoc,
to-plus-from-simp,
toinf-inf,
|
| cons-from-addnum | proved | all subs proved
| append-assoc,
from-succ-cons,
|
| hd-append | proved | all subs proved
| append-assoc,
hd-lem,
cons-append,
elim-hd-tl,
|
| get-cons-num | proved | all subs proved
| append-assoc,
get-cons-succ,
|
| to-unwind-begin | proved | all subs proved
| append-assoc,
append-cancel-l,
get-cons-zero,
to-succ-cons,
size-empty,
elim-hd-tl,
cons-append,
|
| leq-refl | proved | all subs proved
| append-assoc,
appendend-equal,
prefix-def,
|
| to-plus-from | proved | all subs proved
| append-assoc,
to-plus-from-simp,
|
| cons-from-num | proved | all subs proved
| append-assoc,
from-succ-cons,
|
| to-plus-from-fin-simp | proved | all subs proved
| elim-fromto-fin,
|
| cons-to-addnum | proved | all subs proved
| append-assoc,
append-cancel-l,
cons-append,
to-succ-cons,
|
| hd-selzero | proved | all subs proved
| append-assoc,
get-cons-zero,
cons-append,
elim-hd-tl,
|
| to-plus-from-inf | proved | all subs proved
| append-assoc,
finp-append-02,
elim-fromto-inf,
|
| expand-cons | proved | all subs proved
| one-inf,
fun-nonempty,
append-finfin,
fin-empty,
|
| elim-fromto-inf | proved | all subs proved
| append-fininf,
size-fin,
from-inf,
to-inf,
size-inf,
elim-fromto,
|
| elim-fromto-fin | proved | all subs proved
| to-plus-from-fin,
append-from-size,
append-to-size,
length-to,
elim-fromto,
|
| get-cons-zero | proved | all subs proved
| sel-inf,
one-inf,
append-assoc,
get-append2-fin,
|
| get-cons-succ | proved | all subs proved
| one-inf,
sel-inf,
sel-fin,
append-assoc,
get-append2-fin,
|
| to-succ-cons | proved | all subs proved
| to-succ-nf,
eq-stream-to-list-2-1,
one-inf,
to-inf,
append-assoc,
append-cancel-l,
to-fin,
append-finfin,
to-succ-cons-l-lem,
to-appfin,
cons-append,
|
| appendend-equal | proved | all subs proved
| size-fin,
append-assoc,
append-cancel-l-02,
notfin-sizeinf,
|
| elim-hd-tl | proved | all subs proved
| one-inf,
fun-nonempty,
tl-inf,
hd-inf,
append-cancel-l,
append-finfin,
fin-empty,
append-assoc,
tl-lem,
hd-lem,
cons-append,
|
| to-plus-from-simp | proved | all subs proved
| elim-fromto,
|
| from-succ-cons | proved | all subs proved
| get-from-inf,
from-nf,
from-inf,
one-inf,
from-fin,
append-assoc,
from-succ-cons-l-lem,
from-appfin,
|
| to-is-prefix | proved | all subs proved
| append-assoc,
leq-append-right,
size-append,
elim-fromto,
|
| from-succ | proved | all subs proved
| get-from-inf,
one-inf,
from-nf,
size-inf,
from-inf,
sel-inf,
from-zero-l,
from-succ-cons-l-lem,
size-fin,
append-assoc,
eq-stream-to-list-2-1,
from-fin,
sel-fin,
cons-append,
|
| from-cons-one | proved | all subs proved
| from-nf,
from-inf,
one-inf,
from-cons-one-fin,
from-fin,
append-finfin,
|
| append-cancel-l-02 | proved | all subs proved
| neq-fin-inf-01,
fun-nonempty,
append-inf,
append-assoc,
append-empty,
empty,
eq-stream-to-list-2-1,
fin-empty,
|
| elim-fromto | proved | all subs proved
| get-infto,
size-inf-to,
from-nf,
append-fininf,
neq-fin-inf-03,
size-inf,
from-inf,
to-inf,
inf-size-to,
to-plus-from-inf-simp,
append-inf,
neq-fin-inf-01,
append-from-size,
append-to-size,
length-to,
size-fin,
append-assoc,
to-plus-from-fin,
eq-stream-to-list-2-1,
from-fin,
to-fin,
|
| one-inf | proved | all subs proved
| append-assoc,
append-cancel-l,
cons-append,
intrace-expand,
|
| append-cancel-r-02 | proved | all subs proved
| append-inf,
fun-nonempty,
fin-empty,
eq-stream-to-list-2-1,
append-assoc,
empty-append,
|
| append-cancel-r-04 | proved | all subs proved
| fun-nonempty,
append-inf,
append-assoc,
empty-append,
empty,
fin-empty,
eq-stream-to-list-2-1,
|
| fin-neq-inf | proved | all subs proved
| append-assoc,
neq-fin-inf-01,
cons-append,
|
| eq-stream-to-list-3-1 | proved | all subs proved
| eq-stream-to-list-2-1,
append-assoc,
append-cancel-l,
append-finfin,
|
| cons-eq-inf | proved | all subs proved
| append-fininf,
append-assoc,
neq-fin-inf-03,
cons-append,
|
| append-split | proved | all subs proved
| append-inf,
size-inf,
cons-eq,
append-finfin,
empty-append,
empty,
neq-fin-inf-01,
neq-fin-inf-02,
append-assoc,
eq-stream-to-list-2-2,
size-fin,
|
| cons-append | proved | all subs proved
| append-fininf,
cons-inf,
append-assoc,
append-cancel-l,
cons-fin,
append-finfin,
|
| eq-stream-to-list-2-1 | proved | all subs proved
| append-assoc,
append-cancel-l,
append-finfin,
|
| append-extract-list-2 | proved | all subs proved
| append-assoc,
append-extract-list,
|
| leq-append-both | proved | all subs proved
| append-assoc,
append-cancel-l,
leq-append-right,
prefix-def,
|
| append-cut1 | proved | all subs proved
| append-inf,
size-inf,
size-fin,
append-assoc,
append-cancel-l,
|
| toinf-to-eq-inf | proved | all subs proved
| toinf-to-eq,
size-inf,
|
| toinf-to-eq | proved | all subs proved
| toinf-fin,
to-to-eq,
toinf-inf,
|
| cons-eq | proved | all subs proved
| neq-fin-inf-03,
append-fininf,
neq-fin-inf-01,
neq-fin-inf-02,
append-assoc,
eq-stream-to-list-2-2,
|
| append-extract-list | proved | all subs proved
| cons-extract-list,
finp-append-02,
append-finfin,
append-assoc,
empty-append,
empty,
|
| append-cancel-l | proved | all subs proved
| append-fininf,
neq-fin-inf-01,
neq-fin-inf-02,
append-assoc,
eq-stream-to-list-2-2,
|
| swap-inf-to-from | proved | all subs proved
| swap-inf-from-to,
|
| empty-leq | proved | all subs proved
| append-assoc,
append-empty-01,
prefix-def,
leq-empty,
|
| swap-inf-to-from-app | proved | all subs proved
| to-inf,
from-inf,
size-inf,
swap-to-from-app,
|
| toinf-to-ls | proved | all subs proved
| to-to-ls,
toinf-fin,
toinf-inf,
|
| cons-empty | proved | all subs proved
| append-assoc,
fin-empty,
append-empty-01,
|
| toinf-to-leq-inf | proved | all subs proved
| to-inf,
toinf-to-leq,
size-inf,
|
| toinf-to-leq | proved | all subs proved
| to-to-leq,
toinf-fin,
toinf-inf,
|
| to-to-eq | proved | all subs proved
| to-to-leq,
|
| to-to-ls | proved | all subs proved
| to-to-leq,
|
| to-append-add | proved | all subs proved
| get-append-notls,
get-append-ls,
get-to,
append-assoc,
size-to,
size-append,
extensionality,
|
| swap-to-from-app | proved | all subs proved
| sel-inf,
inf-size-from,
get-to,
get-append-notls,
get-append-ls,
sel-fin,
inf-not-to,
neq-fin-inf-03,
fin-size-from2,
less-size-from,
size-from-less,
size-inf-to,
to-inf,
inf-size-to,
from-inf,
size-inf,
length-to,
length-from,
from-appfin,
to-fin,
from-fin,
size-fin,
size-to,
get-from,
append-assoc,
size-append,
extensionality,
|
| neq-fin-inf-02 | proved | all subs proved
| neq-fin-inf-03,
append-fininf,
append-assoc,
append-inf,
|
| finp-append-02 | proved | all subs proved
| neq-fin-inf-01,
append-assoc,
neq-fin-inf-03,
|
| append-empty-01 | proved | all subs proved
| append-inf,
fun-nonempty,
append-fininf,
empty,
append-finfin,
fin-empty,
append-assoc,
append-empty,
|
| swap-inf-from-to | proved | all subs proved
| from-fin,
to-inf,
from-inf,
size-inf,
swap-from-to,
|
| from-append-tofrom | proved | all subs proved
| get-from,
get-append-notls,
get-append-ls,
get-to,
size-inf,
from-inf,
size-fin,
length-from,
from-fin,
append-assoc,
size-to,
size-append,
extensionality,
|
| from-append-add | proved | all subs proved
| inf-not-to,
neq-fin-inf-03,
get-from-01,
neq-fin-inf-01,
get-append-ls,
get-append-notls,
get-from-inf,
sel-inf,
from-inf,
size-to,
size-append,
less-size-from,
size-inf-to,
to-inf,
size-inf,
append-from-gt,
length-to,
append-assoc,
from-appfin,
to-fin,
fin-empty,
from-all,
size-empty-equiv,
size-fin,
sel-fin,
from-fin,
length-from,
fin-size-from,
extensionality,
|
| size-inf-toinf | proved | all subs proved
| size-toinf,
size-inf,
|
| append-notsmallersize1 | proved | all subs proved
| append-assoc,
size-append,
|
| tl-one | proved | all subs proved
| empty,
append-assoc,
append-empty,
tl-fin-lem,
|
| prefix-notsmallersize | proved | all subs proved
| append-assoc,
size-append,
prefix-def,
|
| append-eq-inf | proved | all subs proved
| append-assoc,
append-inf,
neq-fin-inf-03,
|
| swap-to-from | proved | all subs proved
| swap-from-to,
|
| contractinf-tl | proved | all subs proved
| sel-fin,
get-append-notls,
get-append-ls,
sel-inf,
append-assoc,
size-inf,
size-fin,
size-append,
extensionality,
tl-inf,
|
| append-notsmallersize2 | proved | all subs proved
| append-assoc,
size-append,
|
| get-fintoinf | proved | all subs proved
| sel-fin,
get-toinf,
size-fin,
|
| finp-append-01 | proved | all subs proved
| append-assoc,
neq-fin-inf-03,
|
| contractinf-from1 | proved | all subs proved
| sel-fin,
get-from-inf,
get-append-notls,
get-append-ls,
sel-inf,
append-assoc,
size-inf,
size-fin,
size-append,
extensionality,
|
| get-inftoinf | proved | all subs proved
| sel-inf,
get-toinf,
size-inf,
|
| hd-one | proved | all subs proved
| append-assoc,
append-empty,
empty,
hd-fin-lem,
|
| get-toinf | proved | all subs proved
| get-to,
toinf-fin,
toinf-inf,
|
| swap-from-to | proved | all subs proved
| get-from,
get-to,
get-infto,
inf-size-to,
to-inf,
from-inf,
size-inf-to,
get-from-inf,
size-fin,
length-from,
from-fin,
to-fin,
get-finto,
get-from-01,
length-to,
sel-fin,
fin-size-from,
size-to,
extensionality,
|
| to-to-leq | proved | all subs proved
| to-inf,
to-to-leq-inf,
length-to,
append-to-le,
to-unwind-end-fin,
to-zero-l,
size-fin,
to-fin,
|
| leq-empty | proved | all subs proved
| append-assoc,
empty-append,
prefix-def,
|
| append-from-size | proved | all subs proved
| from-zero-l,
append-from-addsize,
|
| tl-lem | proved | all subs proved
| tl-inf,
append-fininf,
append-assoc,
tl-fin-lem,
|
| hd-lem | proved | all subs proved
| hd-inf,
append-fininf,
append-assoc,
hd-fin-lem,
|
| size-toinf | proved | all subs proved
| size-to,
toinf-fin,
toinf-inf,
|
| size-append | proved | all subs proved
| append-assoc,
append-inf,
size-inf,
append-fininf,
append-finfin,
size-fin,
|
| get-append-notls | proved | all subs proved
| size-inf,
append-inf,
append-fininf,
sel-inf,
sel-fin,
append-assoc,
get-append2-fin,
size-fin,
|
| get-append-ls | proved | all subs proved
| append-inf,
sel-inf,
append-fininf,
append-assoc,
get-append2-fin,
size-fin,
sel-fin,
|
| neq-fin-inf-03 | proved | all subs proved
| append-finfin,
append-assoc,
append-inf,
|
| append-empty | proved | all subs proved
| append-assoc,
append-inf,
append-finfin,
empty,
|
| neq-fin-inf-01 | proved | all subs proved
| append-assoc,
append-inf,
append-fininf,
|
| ton-fromn | proved | all subs proved
| empty,
ton-fromn-inf,
to-inf,
ton-fromn-fin,
size-fin,
fin-empty,
from-fin,
to-fin,
|
| append-to-addsize | proved | all subs proved
| to-zero-l,
append-to-size,
append-to-gr,
|
| get-from-zero | proved | all subs proved
| get-from,
|
| append-cancel-r-01 | proved | all subs proved
| append-assoc,
eq-stream-to-list-2-2,
|
| lslen-fromnotempty | proved | all subs proved
| fun-nonempty,
from-inf,
lslen-fromnotempty-list,
size-fin,
fin-empty,
from-fin,
|
| to-to-eq-inf | proved | all subs proved
| to-to-leq-inf,
|
| constrrew | proved | all subs proved
| append-assoc,
eq-stream-to-list-2-2,
append-finfin,
|
| to-from-01 | proved | all subs proved
| empty,
ton-fromn-inf,
to-inf,
from-succ-cons-l-lem,
to-succ-cons-l-lem,
from-zero-l,
to-zero-l,
size-fin,
fin-empty,
from-fin,
to-fin,
|
| leq-append-left | proved | all subs proved
| append-assoc,
leq-append-right,
prefix-def,
|
| tl-fin-1 | proved | all subs proved
| append-assoc,
tl-fin-lem,
append-finfin,
|
| leq-trans | proved | all subs proved
| append-assoc,
prefix-def,
|
| finlen-tolen | proved | all subs proved
| size-inf,
to-all,
to-fin,
size-fin,
|
| size-from-less | proved | all subs proved
| size-inf,
from-inf,
size-fin,
length-from,
from-fin,
|
| fin-size-from2 | proved | all subs proved
| size-fin,
length-from,
from-fin,
|
| append-from-addsize | proved | all subs proved
| from-all,
append-from-le,
from-zero-l,
append-from-gt,
|
| to-to-leq-inf | proved | all subs proved
| to-unwind-end-fin,
size-inf-to,
append-to-le,
to-unwind-end-inf,
to-zero-nf,
to-zero-l,
|
| lslen-fromnotempty-list | proved | all subs proved
| length-from,
|
| to-empty-fin2 | proved | all subs proved
| length-to,
to-zero-l,
|
| append-to-size | proved | all subs proved
| to-all,
append-to-le,
|
| get-to | proved | all subs proved
| sel-inf,
get-infto,
to-inf,
sel-fin,
get-finto,
size-fin,
to-fin,
|
| get-from | proved | all subs proved
| sel-inf,
get-from-inf,
from-inf,
sel-fin,
get-from-01,
size-fin,
from-fin,
|
| ton-fromn-fin | proved | all subs proved
| length-to,
length-from,
|
| ton-fromn-inf | proved | all subs proved
| size-inf-to,
length-from,
|
| fin-size-from | proved | all subs proved
| size-fin,
length-from,
from-fin,
|
| less-size-from | proved | all subs proved
| size-inf,
from-inf,
size-fin,
length-from,
from-fin,
|
| size-to | proved | all subs proved
| inf-size-to,
to-inf,
length-to,
size-fin,
to-fin,
|
| append-assoc | proved | all subs proved
| append-inf,
append-fininf,
eq-stream-to-list-3-3,
append-finfin,
|
| fin-toinf | proved | all subs proved
| inf-not-toinf-exceptinf,
toinf-inf,
|
| size-to-02 | proved | all subs proved
| size-inf-to,
to-inf,
length-to,
size-fin,
to-fin,
|
| get-to-02 | proved | all subs proved
| sel-inf,
get-infto,
to-inf,
sel-fin,
get-finto,
size-fin,
to-fin,
|
| fin-finlen-tolen | proved | all subs proved
| to-all,
|
| toinflen | proved | all subs proved
| toinf-inf,
size-inf,
to-all,
to-fin,
toinf-fin,
size-fin,
|
| from-cons-one-fin | proved | all subs proved
| from-zero-l,
from-succ-cons-l-lem,
|
| append-from-le | proved | all subs proved
| from-succ-cons-l-lem,
from-zero-l,
|
| to-unwind-end-inf | proved | all subs proved
| to-succ-nf,
to-zero-nf,
to-inf-one,
|
| append-to-le | proved | all subs proved
| to-succ-cons-l-lem,
to-zero-l,
|
| toone-equal | proved | all subs proved
| to-inf-one,
to-inf,
sel-inf,
toone-cons-fin,
fin-empty,
sel-fin,
to-fin,
|
| to-unwind-end-fin | proved | all subs proved
| to-zero-l,
to-succ-cons-l-lem,
|
| eq-stream-to-list-3-3 | proved | all subs proved
| eq-stream-to-list-2-2,
append-finfin,
|
| to-all | proved | all subs proved
| to-succ-cons-l-lem,
to-zero-l,
|
| append-to-gr | proved | all subs proved
| to-succ-cons-l-lem,
|
| to-plus-from-fin | proved | all subs proved
| from-succ-cons-l-lem,
to-succ-cons-l-lem,
from-zero-l,
to-zero-l,
|
| to-plus-from-inf-simp | proved | all subs proved
| get-from-inf,
size-inf-to,
get-infto,
append-fininf,
|
| inf-not-toinf-exceptinf | proved | all subs proved
| inf-not-to,
toinf-fin,
toinf-inf,
|
| single-to-one | proved | all subs proved
| to-zero-l,
to-succ-cons-l-lem,
|
| get-finto | proved | all subs proved
| to-succ-cons-l-lem,
to-zero-l,
|
| inf-size-to | proved | all subs proved
| size-inf-to,
size-fin,
|
| size-empty-equiv | proved | all subs proved
| size-inf,
fin-empty,
size-fin,
size-empty,
|
| from-all | proved | all subs proved
| from-succ-cons-l-lem,
from-zero-l,
|
| length-to | proved | all subs proved
| to-succ-cons-l-lem,
to-zero-l,
|
| append-from-gt | proved | all subs proved
| from-succ-cons-l-lem,
|
| get-from-01 | proved | all subs proved
| from-succ-cons-l-lem,
from-zero-l,
|
| length-from | proved | all subs proved
| from-succ-cons-l-lem,
from-zero-l,
|
| from-zero | proved | all subs proved
| from-nf-zero,
from-inf,
from-zero-l,
from-fin,
|
| get-append3-fin | proved | all subs proved
| get-append2-fin,
append-finfin,
|
| finp-to | proved | all subs proved
| fin-to,
|
| to-unwind-begin-fin | proved | all subs proved
| to-succ-cons-l-lem,
|
| from-from | proved | all subs proved
| get-from-inf,
from-nf,
size-inf,
from-inf,
from-succ-cons-l-lem,
from-zero-l,
size-fin,
from-fin,
|
| finp-empty | proved | all subs proved
| fin-empty,
|
| from-from-inf | proved | all subs proved
| get-from-inf,
|
| zero-len | proved | all subs proved
| size-inf,
fun-nonempty,
size-fin,
fin-empty,
|
| intrace-expand | proved | all subs proved
| cons-inf,
|
| from-nf-zero | proved | all subs proved
| from-nf,
|
| inf-size-from | proved | all subs proved
| size-inf,
from-inf,
size-fin,
|
| hd-fin-lem | proved | all subs proved
| hd-fin,
append-finfin,
|
| toone-cons-fin | proved | all subs proved
| to-zero-l,
to-succ-cons-l,
|
| notfin-sizeinf | proved | all subs proved
| size-inf,
|
| to-appfin | proved | all subs proved
| to-fin,
append-finfin,
|
| eq-stream-to-list-2-2 | proved | all subs proved
| append-finfin,
|
| cons-extract-list | proved | all subs proved
| append-finfin,
|
| leq-append-right | proved | all subs proved
| prefix-def,
|
| size-empty | proved | all subs proved
| size-fin,
empty,
|
| size-succ | proved | all subs proved
| size-inf,
size-fin,
|
| tl-fin-lem | proved | all subs proved
| tl-fin,
append-finfin,
|
| fin-to | proved | all subs proved
| finp-infto,
to-inf,
to-fin,
|
| get-append2-fin | proved | all subs proved
| sel-fin,
append-finfin,
|
| to-inf-one | proved | all subs proved
| to-zero-nf,
to-succ-nf,
|
| get-infto | proved | all subs proved
| to-succ-nf,
to-zero-nf,
|
| to-zero | proved | all subs proved
| to-zero-nf,
to-inf,
empty,
to-zero-l,
to-fin,
|
| to-succ-cons-l-lem | proved | all subs proved
| to-succ-cons-l,
|
| extensionality | proved | all subs proved
| sel-inf,
size-inf,
sel-fin,
size-fin,
|
| from-appfin | proved | all subs proved
| from-fin,
append-finfin,
|
| get-from-inf | proved | all subs proved
| from-nf,
|
| inf-not-to | proved | all subs proved
| to-inf,
to-fin,
|
| size-inf-to | proved | all subs proved
| to-succ-nf,
to-zero-nf,
|
| fin-empty | proved | all subs proved
| empty,
|
| fun-nonempty | proved | all subs proved
| empty,
|
| toinf-add | proved | all subs proved
| toinf-fin,
|
| empty-append | proved | all subs proved
| append-fininf,
append-finfin,
empty,
|
| from-succ-cons-l-lem | proved | all subs proved
| from-succ-cons-l,
|
| get-from-inf-zero | proved | all subs proved
| from-nf,
|
| eq-stream-to-list-3-2 | proved | all subs proved
| append-finfin,
|
| extract-empty | proved | all subs proved
| empty,
|
| nlslen-lslensn-eqlensn | proved | all subs proved
| size-inf,
size-fin,
|
| size-from-inf | proved | all subs proved
| size-inf,
from-inf,
|
| tl-inf-1 | proved | all subs proved
| tl-inf,
cons-inf,
|
| cons-fin | axiom | | |
| finp-infto | proved | all subs proved
| |
| from-succ-cons-l | axiom | | |
| cons-inf | axiom | | |
| tl-fin | axiom | | |
| append-fininf | axiom | | |
| hd-inf | axiom | | |
| tl-inf | axiom | | |
| prefix-def | axiom | | |
| to-zero-nf | axiom | | |
| to-succ-nf | axiom | | |
| to-succ-cons-l | axiom | | |
| to-zero-l | axiom | | |
| hd-fin | axiom | | |
| from-nf | axiom | | |
| from-fin | axiom | | |
| sel-fin | axiom | | |
| size-fin | axiom | | |
| to-fin | axiom | | |
| size-inf | axiom | | |
| to-inf | axiom | | |
| from-inf | axiom | | |
| sel-inf | axiom | | |
| append-inf | axiom | | |
| toinf-inf | axiom | | |
| toinf-fin | axiom | | |
| from-zero-l | axiom | | |
| empty | axiom | | |
| append-finfin | axiom | | |