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: |
|---|
| toinftoinf-append-add | proved | all subs proved
| toinf-fin,
append-assoc,
toinfto-append-add,
toinf-inf,
|
| toinfto-append-add | proved | all subs proved
| append-split-fin,
toinf-fin,
append-finfin,
to-append-add,
toinf-add,
append-assoc,
to-empty2,
fin-empty,
appendend-equal,
toinf-inf,
append-toinf-ls,
|
| toinf-to-eq-inf | proved | all subs proved
| toinf-to-eq,
size-inf,
|
| to-append-add | proved | all subs proved
| to-zero,
to-to-eq,
size-to,
size-to-02,
append-assoc,
to-fin,
append-le-to,
append-gr-to,
|
| toinf-to-eq | proved | all subs proved
| toinf-fin,
to-to-eq,
to-fin,
toinf-inf,
|
| toinf-to-ls | proved | all subs proved
| to-to-ls,
to-fin,
toinf-fin,
toinf-inf,
|
| fin-to-to-ls | proved | all subs proved
| to-fin,
size-fin,
to-to-ls,
|
| toinf-to-leq-inf | proved | all subs proved
| to-inf,
toinf-to-leq,
size-inf,
|
| toinf-empty3 | proved | all subs proved
| to-empty3,
fin-empty,
toinf-add,
toinf-inf,
|
| fin-to-to-eq | proved | all subs proved
| to-fin,
size-fin,
to-to-eq,
|
| to-empty3 | proved | all subs proved
| size-succ,
to-empty2,
|
| toinf-to-leq | proved | all subs proved
| to-to-leq,
to-fin,
toinf-fin,
toinf-inf,
|
| to-to-ls | proved | all subs proved
| to-to-leq,
|
| to-to-eq | proved | all subs proved
| to-to-leq,
|
| to-empty4 | proved | all subs proved
| size-empty-equiv,
to-empty2,
|
| toinf-empty | proved | all subs proved
| to-empty,
fin-empty,
toinf-inf,
empty,
to-zero,
toinf-fin,
|
| appinf-to-ge-01 | proved | all subs proved
| append-assoc,
fin-finlen-tolen,
appinf-to-split,
appinf-to-ge,
|
| toinf-empty2 | proved | all subs proved
| to-empty2,
fin-empty,
size-empty,
toinf-inf,
empty,
to-zero,
toinf-fin,
|
| fin-to-to-leq | proved | all subs proved
| to-fin,
size-fin,
to-to-leq,
|
| appinf-to-ge | proved | all subs proved
| to-empty-inf,
fin-finlen-tolen,
appinf-to-split,
|
| to-empty | proved | all subs proved
| to-empty-inf,
to-inf,
to-empty-fin,
size-fin,
to-fin,
to-zero,
|
| to-empty2 | proved | all subs proved
| to-empty-inf,
to-inf,
to-empty-fin2,
size-fin,
to-fin,
to-zero,
|
| to-to-leq | proved | all subs proved
| to-inf,
to-to-leq-inf,
size-fin,
to-fin,
|
| toinf-empty-inf | proved | all subs proved
| to-empty-inf,
fin-empty,
fun-nonempty,
toinf-inf,
empty,
to-zero-nf,
to-inf,
toinf-fin,
|
| to-to-eq-inf | proved | all subs proved
| to-to-leq-inf,
|
| to-to-leq-inf | proved | all subs proved
| to-inf-one,
infapp-to-ge-01,
append-assoc,
appinf-sel,
infapp-get-eq,
elim-fromto-inf,
size-inf-to,
to-unwind-end-inf,
to-zero-nf,
|
| to-empty-inf | proved | all subs proved
| elim-fromto-inf,
to-zero-nf,
|
| from-append-toinffrom | proved | all subs proved
| from-append-tofrom,
eq-stream-to-list-2-1,
toinf-add,
toinf-fin,
append-assoc,
to-plus-from-simp,
toinf-inf,
|
| infapp-to-eq | proved | all subs proved
| infapp-inj,
append-assoc,
appinf-sel,
elim-fromto-inf,
|
| swap-inf-to-from-app | proved | all subs proved
| to-inf,
from-inf,
size-inf,
swap-to-from-app,
|
| to-plus-from | proved | all subs proved
| append-assoc,
to-plus-from-simp,
|
| infapp-from-eqadd | proved | all subs proved
| infapp-inj,
infapp-assoc,
append-assoc,
appinf-sel,
elim-fromto-inf,
|
| infapp-from-eq | proved | all subs proved
| infapp-inj,
append-assoc,
appinf-sel,
elim-fromto-inf,
|
| swap-to-from-app | proved | all subs proved
| empty-append,
empty,
to-zero,
from-zero,
append-assoc,
append-split-fin,
swap-to-from,
append-from-le-01,
size-to,
size-to-02,
append-from-ge-02,
|
| elim-fromto-inf | proved | all subs proved
| append-assoc,
append-split-fin,
appinf-selfun,
size-inf-to,
from-inf,
to-inf,
size-inf,
elim-fromto,
|
| to-plus-from-simp | proved | all subs proved
| elim-fromto,
|
| to-is-prefix | proved | all subs proved
| append-assoc,
leq-append-right,
size-fin,
size-append,
size-empty-equiv,
elim-fromto,
|
| swap-inf-to-from | proved | all subs proved
| swap-inf-from-to,
|
| swap-inf-from-to | proved | all subs proved
| to-inf,
from-inf,
size-inf,
swap-from-to,
|
| append-toinf-ls | proved | all subs proved
| toinf-fin,
append-le-to,
append-assoc,
appendend-equal,
toinf-inf,
|
| elim-fromto | proved | all subs proved
| to-plus-from-inf-simp,
from-inf,
to-inf,
size-fin,
eq-stream-to-list-2-1,
from-fin,
to-fin,
append-assoc,
append-from-size-01,
append-to-size-01,
size-to,
|
| append-from-ge-02 | proved | all subs proved
| size-inf,
append-assoc,
append-from-size-01,
size-fin,
from-zero,
append-from-gr-02,
|
| swap-to-from | proved | all subs proved
| swap-from-to,
|
| append-gr-to | proved | all subs proved
| size-inf,
to-inf,
append-inf,
append-assoc,
append-to-gr-01,
size-fin,
|
| append-to-addsize-01 | proved | all subs proved
| to-zero,
append-assoc,
append-to-size-01,
append-to-gr-01,
|
| toone-one | proved | all subs proved
| single-to-one,
to-fin,
append-assoc,
append-empty,
toone-cons,
|
| leq-prefix | proved | all subs proved
| finlen-tolen,
append-le-to,
size-empty-equiv,
append-assoc,
size-append,
appendend-equal,
prefix-def,
|
| to-unwind-end2 | proved | all subs proved
| to-unwind-end,
|
| extensionality-to | proved | all subs proved
| to-unwind-end,
size-succ,
extensionality,
|
| to-attach | proved | all subs proved
| append-assoc,
append-to-size-01,
cons-to-addnum,
append-finfin,
to-fin,
|
| append-from-gr-02 | proved | all subs proved
| size-inf,
from-inf,
append-inf,
append-assoc,
append-from-gr-01,
size-fin,
|
| to-unwind-end | proved | all subs proved
| to-succ-nf,
to-zero-nf,
to-inf-one,
fun-nonempty,
one-inf,
size-inf,
sel-inf,
to-inf,
to-unwind-end-fin,
sel-fin,
to-fin,
size-succ,
get-cons-succ,
get-cons-zero,
to-zero,
cons-to-num,
append-assoc,
size-fin,
size-append,
to-succ-cons,
size-empty,
expand-cons,
|
| toone-cons | proved | all subs proved
| to-zero-nf,
to-inf,
append-assoc,
to-fin,
cons-to-num,
|
| append-to-gr-01 | proved | all subs proved
| to-zero,
cons-to-num,
append-finfin,
append-assoc,
empty-append,
empty,
|
| append-to-size-01 | proved | all subs proved
| fin-finlen-tolen,
append-to-le-01,
|
| swap-from-to | proved | all subs proved
| from-to-exchange,
|
| append-le-to | proved | all subs proved
| to-inf,
append-inf,
append-assoc,
append-to-le-01,
size-fin,
to-fin,
|
| leq-symm | proved | all subs proved
| leq-symm-2,
|
| from-infto-exchange | proved | all subs proved
| from-to-exchange,
toinf-fin,
from-fin,
toinf-add,
toinf-inf,
|
| append-from-ge-01 | proved | all subs proved
| from-zero,
append-assoc,
append-from-size-01,
append-from-gr-01,
|
| append-from-gr-01 | proved | all subs proved
| append-assoc,
append-from-addsize-01,
|
| from-to-exchange | proved | all subs proved
| append-assoc,
size-fin,
size-append,
cons-append,
cons-from-addnum,
cons-to-addnum,
size-empty,
elim-hd-tl,
from-zero,
|
| append-to-le-01 | proved | all subs proved
| cons-to-addnum,
append-finfin,
to-zero,
append-assoc,
empty-append,
empty,
|
| append-from-size-01 | proved | all subs proved
| from-zero,
append-from-addsize-01,
|
| leq-symm-2 | proved | all subs proved
| append-assoc,
prefixself-equal,
appendend-equal,
prefix-def,
|
| cons-to-num | proved | all subs proved
| append-assoc,
cons-to-addnum,
|
| append-from-le-01 | proved | all subs proved
| cons-from-addnum,
append-split-fin,
append-finfin,
append-assoc,
empty-append,
empty,
from-zero,
|
| prefix-inf-id | proved | all subs proved
| append-assoc,
append-to-inf-id,
prefix-def,
leq-refl,
|
| prefix-inf-inf-equal | proved | all subs proved
| append-assoc,
append-inf,
prefix-def,
leq-refl,
|
| prefixself-equal | proved | all subs proved
| append-assoc,
append-empty-01,
empty-append,
appendend-equal,
prefix-def,
|
| leq-refl | proved | all subs proved
| append-assoc,
appendend-equal,
prefix-def,
|
| append-to-inf-id | proved | all subs proved
| append-assoc,
appendend-equal,
|
| cons-to-addnum | proved | all subs proved
| append-assoc,
to-succ-cons,
|
| cons-from-addnum | proved | all subs proved
| append-assoc,
from-succ-cons,
|
| append-from-addsize-01 | proved | all subs proved
| from-succ-cons,
append-finfin,
append-assoc,
empty-append,
empty,
|
| cons-from-num | proved | all subs proved
| append-assoc,
from-succ-cons,
|
| append-prefix-fin-is-fin | proved | all subs proved
| not-prefix-appinf-fin,
not-prefix-inf-fin,
append-inf,
append-assoc,
prefix-appendbothfin-listprefix,
|
| hd-append | proved | all subs proved
| append-assoc,
hd-lem,
cons-append,
elim-hd-tl,
|
| hd-selzero | proved | all subs proved
| append-assoc,
get-cons-zero,
cons-append,
elim-hd-tl,
|
| to-unwind-begin | proved | all subs proved
| append-assoc,
get-cons-zero,
cons-append,
to-succ-cons,
size-empty,
elim-hd-tl,
|
| get-cons-num | proved | all subs proved
| append-assoc,
get-cons-succ,
|
| 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,
|
| prefix-appendbothfin-listprefix | proved | all subs proved
| neq-fin-inf-01,
eq-stream-to-list-3-1,
append-assoc,
append-split-fin,
append-finfin,
prefix-def,
|
| 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,
|
| appendend-equal | proved | all subs proved
| size-fin,
size-inf,
append-assoc,
append-cancel-l-02,
|
| expand-cons | proved | all subs proved
| one-inf,
fun-nonempty,
append-finfin,
fin-empty,
|
| to-succ-cons | proved | all subs proved
| to-succ-nf,
one-inf,
to-inf,
to-fin,
append-assoc,
to-succ-cons-l-lem,
to-appfin,
|
| 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,
|
| from-succ | proved | all subs proved
| get-from-inf,
one-inf,
from-nf,
size-inf,
from-inf,
sel-inf,
size-fin,
append-assoc,
eq-stream-to-list-2-1,
from-fin,
sel-fin,
cons-append,
|
| appfin-sel-01 | proved | all subs proved
| eq-stream-to-list-3-1,
append-assoc,
neq-fin-inf-03,
|
| 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,
|
| eq-stream-to-list-3-1 | proved | all subs proved
| eq-stream-to-list-2-1,
append-assoc,
append-split-fin,
append-finfin,
|
| one-inf | proved | all subs proved
| append-assoc,
append-split-fin,
cons-append,
intrace-expand,
|
| prefix-bothfin-listprefix | proved | all subs proved
| neq-fin-inf-01,
eq-stream-to-list-2-1,
append-assoc,
append-split-fin,
append-finfin,
prefix-def,
|
| append-two-is-fin | proved | all subs proved
| append-inf,
neq-fin-inf-01,
append-assoc,
append-split-fin,
append-finfin,
eq-stream-to-list-2-1,
|
| appfin-sel | proved | all subs proved
| eq-stream-to-list-2-1,
append-assoc,
neq-fin-inf-03,
|
| cons-eq-inf | proved | all subs proved
| append-fininf,
append-assoc,
neq-fin-inf-03,
cons-append,
|
| fin-neq-inf | proved | all subs proved
| append-assoc,
neq-fin-inf-01,
cons-append,
|
| append-fin-is-inf | proved | all subs proved
| append-split-fin,
infapp-embed,
append-fin-inf-fun,
append-assoc,
neq-fin-inf-03,
|
| cons-eq-01 | proved | all subs proved
| neq-fin-inf-01,
fin-empty,
eq-stream-to-list-2-1,
append-assoc,
append-empty,
|
| append-fin-inf-fun | proved | all subs proved
| append-assoc,
append-split-fin,
infapp-embed,
|
| append-cancel-l | proved | all subs proved
| append-assoc,
append-split-fin,
|
| cons-append | proved | all subs proved
| append-fininf,
cons-inf,
append-assoc,
append-split-fin,
cons-fin,
append-finfin,
|
| eq-stream-to-list-2-1 | proved | all subs proved
| append-assoc,
append-split-fin,
append-finfin,
|
| constrrew | proved | all subs proved
| append-assoc,
append-split-fin,
append-finfin,
|
| appinf-selfun-01 | proved | all subs proved
| append-assoc,
append-split-fin,
appinf-selfun,
append-fininf,
|
| append-cut1 | proved | all subs proved
| append-inf,
size-inf,
size-fin,
append-assoc,
append-split-fin,
|
| leq-append-both | proved | all subs proved
| append-assoc,
append-split-fin,
leq-append-right,
prefix-def,
|
| append-split-fin | proved | all subs proved
| size-fin,
append-split,
|
| 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-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,
|
| empty-leq | proved | all subs proved
| append-assoc,
append-empty-01,
prefix-def,
leq-empty,
|
| cons-empty | proved | all subs proved
| append-assoc,
fin-empty,
append-empty-01,
|
| append-empty-01 | proved | all subs proved
| append-inf,
fun-nonempty,
append-fininf,
empty,
append-finfin,
fin-empty,
append-assoc,
append-empty,
|
| neq-fin-inf-02 | proved | all subs proved
| neq-fin-inf-03,
append-fininf,
append-assoc,
append-inf,
|
| not-prefix-appinf-fin | proved | all subs proved
| append-assoc,
neq-fin-inf-01,
append-inf,
prefix-def,
|
| 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,
|
| tl-one | proved | all subs proved
| empty,
append-assoc,
append-empty,
tl-fin-lem,
|
| 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,
|
| append-notsmallersize1 | proved | all subs proved
| append-assoc,
size-append,
|
| appinf-one2-get-zero | proved | all subs proved
| append-assoc,
appinf-one-get-zero,
append-fininf,
|
| appinf-one2-get-succ2 | proved | all subs proved
| append-assoc,
appinf-one-get-succ2,
append-fininf,
|
| appinf-one2-get-succ | proved | all subs proved
| append-assoc,
appinf-one-get-succ,
append-fininf,
|
| appinf-one2-to-succ2 | proved | all subs proved
| append-assoc,
appinf-one-to-succ2,
append-fininf,
|
| hd-one | proved | all subs proved
| append-assoc,
append-empty,
empty,
hd-fin-lem,
|
| from-append-add | proved | all subs proved
| get-from-01,
sel-fin,
from-fin,
from-appfin,
length-from,
size-fin,
get-from-inf,
get-to,
append-fininf,
sel-inf,
size-inf,
from-inf,
get-from,
append-assoc,
size-to,
size-to-02,
size-append,
less-size-from,
fin-size-from,
extensionality,
|
| appinf-one2-to-succ | proved | all subs proved
| append-assoc,
appinf-one-to-succ,
append-fininf,
|
| 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,
|
| size-inf-toinf | proved | all subs proved
| size-toinf,
size-inf,
|
| size-toinf | proved | all subs proved
| size-to,
size-to-02,
toinf-fin,
toinf-inf,
|
| appinf-one-to-succ | proved | all subs proved
| to-zero-nf,
append-assoc,
single-to-one,
appinf-to-split,
|
| infapp-embed | proved | all subs proved
| append-fininf,
append-assoc,
add-list-fun-def,
|
| 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,
|
| appinf-one-to-succ2 | proved | all subs proved
| append-assoc,
appinf-to-split,
|
| leq-empty | proved | all subs proved
| append-assoc,
empty-append,
prefix-def,
|
| appinf-one-get-succ | proved | all subs proved
| append-assoc,
appinf-get-split,
|
| appinf-one-get-succ2 | proved | all subs proved
| append-assoc,
appinf-get-split,
|
| appinf-one-get-zero | proved | all subs proved
| append-assoc,
appinf-get-split,
|
| 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,
|
| not-prefix-inf-fin | proved | all subs proved
| append-assoc,
append-inf,
prefix-def,
|
| get-append-ls | proved | all subs proved
| append-inf,
sel-inf,
append-fininf,
append-assoc,
get-append2-fin,
size-fin,
sel-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,
|
| neq-fin-inf-01 | proved | all subs proved
| append-assoc,
append-inf,
append-fininf,
|
| size-append | proved | all subs proved
| append-assoc,
append-inf,
size-inf,
append-fininf,
append-finfin,
size-fin,
|
| appinf-sel | proved | all subs proved
| add-list-fun-def,
append-fininf,
append-assoc,
|
| inf-take-prefix | proved | all subs proved
| append-assoc,
to-plus-from-inf-simp,
prefix-def,
|
| get-inftoinf | proved | all subs proved
| sel-inf,
get-toinf,
size-inf,
|
| get-fintoinf | proved | all subs proved
| sel-fin,
get-toinf,
size-fin,
|
| tl-fin-1 | proved | all subs proved
| append-assoc,
tl-fin-lem,
append-finfin,
|
| leq-trans | proved | all subs proved
| append-assoc,
prefix-def,
|
| leq-append-left | proved | all subs proved
| append-assoc,
leq-append-right,
prefix-def,
|
| to-plus-from-inf | proved | all subs proved
| append-assoc,
to-plus-from-inf-simp,
|
| finlen-tolen | proved | all subs proved
| size-inf,
size-fin,
finlen-tolen-02,
|
| infapp-assoc | proved | all subs proved
| infapp-get-ls,
infapp-get-ge,
|
| get-toinf | proved | all subs proved
| get-to,
sel-fin,
toinf-fin,
toinf-inf,
|
| from-append-tofrom | proved | all subs proved
| get-from,
get-to,
size-inf,
from-inf,
size-fin,
length-from,
from-fin,
size-to,
|
| size-to-02 | proved | all subs proved
| size-inf-to,
to-inf,
inf-size-to,
to-fin,
size-fin,
|
| append-assoc | proved | all subs proved
| append-inf,
append-fininf,
eq-stream-to-list-3-3,
append-finfin,
|
| ton-fromn | proved | all subs proved
| ton-fromn-inf,
to-inf,
ton-fromn-fin,
size-fin,
to-fin,
|
| to-unwind-end-inf2 | proved | all subs proved
| to-unwind-end-inf,
|
| infapp-to-eqadd | proved | all subs proved
| infapp-to-ge-01,
|
| appinf-to-le | proved | all subs proved
| appinf-to-split,
|
| append-from-size | proved | all subs proved
| append-from-addsize,
|
| get-from-zero | proved | all subs proved
| get-from,
|
| to-from-01 | proved | all subs proved
| ton-fromn-inf,
to-inf,
size-fin,
to-fin,
|
| infapp-to-ge | proved | all subs proved
| infapp-to-ge-01,
|
| finlen-tolen-02 | proved | all subs proved
| size-inf,
fin-finlen-tolen,
to-fin,
size-fin,
|
| inf-size-to | proved | all subs proved
| size-inf-to,
size-fin,
|
| get-from | proved | all subs proved
| sel-inf,
get-from-inf,
from-inf,
sel-fin,
get-from-01,
size-fin,
from-fin,
|
| get-to | proved | all subs proved
| sel-inf,
get-infto,
to-inf,
sel-fin,
get-finto,
size-fin,
to-fin,
|
| eq-stream-to-list-3-3 | proved | all subs proved
| eq-stream-to-list-2-2,
append-finfin,
|
| append-from-addsize | proved | all subs proved
| append-from-gt,
|
| size-empty-equiv | proved | all subs proved
| size-inf,
fin-empty,
size-fin,
size-empty,
|
| appinf-to-split | proved | all subs proved
| get-finto,
length-to,
append-fininf,
get-infto,
size-inf-to,
|
| infapp-get-ge | proved | all subs proved
| infapp-get-eqadd,
|
| infapp-to-ge-01 | proved | all subs proved
| get-infto,
size-inf-to,
add-list-fun-def,
|
| to-unwind-end-inf | proved | all subs proved
| to-succ-nf,
to-zero-nf,
to-inf-one,
|
| ton-fromn-inf | proved | all subs proved
| size-inf-to,
length-from,
|
| from-zero | proved | all subs proved
| from-nf-zero,
from-inf,
from-fin,
|
| size-to | proved | all subs proved
| size-inf-to,
to-inf,
length-to,
size-fin,
to-fin,
|
| to-plus-from-inf-simp | proved | all subs proved
| get-from-inf,
size-inf-to,
get-infto,
append-fininf,
|
| to-inf-two | proved | all subs proved
| get-infto,
size-inf-to,
|
| infapp-from-le | proved | all subs proved
| add-list-fun-def,
get-from-inf,
|
| get-append3-fin | proved | all subs proved
| get-append2-fin,
append-finfin,
|
| infapp-from-gt | proved | all subs proved
| get-from-inf,
from-nf,
add-list-fun-def,
|
| lslen-fromnotempty | proved | all subs proved
| fun-nonempty,
from-inf,
size-fin,
fin-empty,
from-fin,
|
| infapp-to-le | proved | all subs proved
| add-list-fun-def,
get-infto,
size-inf-to,
|
| from-from-inf | proved | all subs proved
| get-from-inf,
|
| toinflen | proved | all subs proved
| toinf-inf,
size-inf,
fin-finlen-tolen,
to-fin,
toinf-fin,
size-fin,
|
| zero-len | proved | all subs proved
| size-inf,
fun-nonempty,
size-fin,
fin-empty,
|
| toone-equal | proved | all subs proved
| to-inf-one,
to-inf,
sel-inf,
fin-empty,
sel-fin,
to-fin,
|
| infapp-one-to-succ2 | proved | all subs proved
| add-list-fun-def,
to-succ2-nf,
|
| from-from | proved | all subs proved
| get-from-inf,
from-nf,
size-inf,
from-inf,
from-fin,
|
| infapp-get-eqadd | proved | all subs proved
| add-list-fun-def,
|
| to-succ2-nf | proved | all subs proved
| to-succ-nf,
|
| from-cons-one-fin | proved | all subs proved
| from-succ-cons-l-lem,
|
| 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,
|
| from-appfin | proved | all subs proved
| from-fin,
append-finfin,
|
| append-from-gt | proved | all subs proved
| from-succ-cons-l-lem,
|
| single-to-one | proved | all subs proved
| to-succ-cons-l-lem,
|
| leq-append-right | proved | all subs proved
| prefix-def,
|
| infapp-get-eq | proved | all subs proved
| add-list-fun-def,
|
| from-nf-zero | proved | all subs proved
| from-nf,
|
| appinf-selfun | proved | all subs proved
| append-fininf,
|
| fin-finlen-tolen | proved | all subs proved
| to-all,
|
| intrace-expand | proved | all subs proved
| cons-inf,
|
| to-appfin | proved | all subs proved
| to-fin,
append-finfin,
|
| hd-fin-lem | proved | all subs proved
| hd-fin,
append-finfin,
|
| eq-stream-to-list-2-2 | proved | all subs proved
| append-finfin,
|
| tl-fin-lem | proved | all subs proved
| tl-fin,
append-finfin,
|
| size-inf-to | proved | all subs proved
| to-succ-nf,
to-zero-nf,
|
| get-infto | proved | all subs proved
| to-succ-nf,
to-zero-nf,
|
| infapp-get-ls | proved | all subs proved
| add-list-fun-def,
|
| extensionality | proved | all subs proved
| sel-inf,
size-inf,
sel-fin,
size-fin,
|
| get-from-inf | proved | all subs proved
| from-nf,
|
| appinf-get-split | proved | all subs proved
| append-fininf,
|
| get-append2-fin | proved | all subs proved
| sel-fin,
append-finfin,
|
| size-succ | proved | all subs proved
| size-inf,
size-fin,
|
| fun-nonempty | proved | all subs proved
| empty,
|
| ton-fromn-fin | proved | all subs proved
| length-to,
length-from,
|
| infapp-inj | proved | all subs proved
| add-list-fun-def,
|
| size-empty | proved | all subs proved
| size-fin,
empty,
|
| fin-empty | proved | all subs proved
| empty,
|
| empty-append | proved | all subs proved
| append-fininf,
append-finfin,
empty,
|
| toinf-add | proved | all subs proved
| toinf-fin,
|
| to-zero | proved | all subs proved
| to-zero-nf,
to-inf,
to-fin,
|
| to-inf-one | proved | all subs proved
| to-zero-nf,
to-succ-nf,
|
| infapp-one-to-succ | proved | all subs proved
| add-list-fun-def,
to-succ-nf,
|
| infappone-zero | proved | all subs proved
| add-list-fun-def,
|
| tl-inf-1 | proved | all subs proved
| tl-inf,
cons-inf,
|
| to-succ3-nf | proved | all subs proved
| to-succ-nf,
|
| get-from-inf-zero | proved | all subs proved
| from-nf,
|
| to-unwind-end-fin2 | proved | all subs proved
| to-unwind-end-fin,
|
| infapp-empty | proved | all subs proved
| add-list-fun-def,
|
| inf-not-toinf-exceptinf | proved | all subs proved
| toinf-fin,
toinf-inf,
|
| appinf-get-ge-01 | proved | all subs proved
| append-fininf,
|
| eq-stream-to-list-3-2 | proved | all subs proved
| append-finfin,
|
| size-from | proved | all subs proved
| size-inf,
from-inf,
size-fin,
length-from,
from-fin,
|
| size-from-less | proved | all subs proved
| size-inf,
from-inf,
size-fin,
length-from,
from-fin,
|
| extract-empty | proved | all subs proved
| empty,
|
| appinf-get-le | proved | all subs proved
| append-fininf,
|
| appinf-get-ge | proved | all subs proved
| append-fininf,
|
| to-unwind-begin-fin | proved | all subs proved
| to-succ-cons-l-lem,
|
| inf-size-from | proved | all subs proved
| size-inf,
from-inf,
size-fin,
|
| size-from-inf | proved | all subs proved
| size-inf,
from-inf,
|
| hd-fin | axiom | | |
| get-finto | proved | all subs proved
| |
| tl-fin | axiom | | |
| to-empty-fin | proved | all subs proved
| |
| cons-fin | axiom | | |
| from-succ-cons-l-lem | proved | all subs proved
| |
| to-succ-cons-l-lem | proved | all subs proved
| |
| hd-inf | axiom | | |
| get-from-01 | proved | all subs proved
| |
| to-empty-fin2 | proved | all subs proved
| |
| length-to | proved | all subs proved
| |
| cons-inf | axiom | | |
| tl-inf | axiom | | |
| from-fin | axiom | | |
| length-from | proved | all subs proved
| |
| from-inf | axiom | | |
| to-all | proved | all subs proved
| |
| sel-fin | axiom | | |
| to-unwind-end-fin | proved | all subs proved
| |
| sel-inf | axiom | | |
| append-inf | axiom | | |
| to-inf | axiom | | |
| add-list-fun-def | axiom | | |
| size-fin | axiom | | |
| size-inf | axiom | | |
| from-nf | axiom | | |
| append-fininf | axiom | | |
| empty | axiom | | |
| append-finfin | axiom | | |
| toinf-inf | axiom | | |
| toinf-fin | axiom | | |
| to-fin | axiom | | |
| prefix-def | axiom | | |
| to-zero-nf | axiom | | |
| to-succ-nf | axiom | | |