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

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:
swap-inf-to-from-appprovedall subs proved to-inf, from-inf, size-inf, swap-to-from-app,
toinftoinf-append-addprovedall subs proved toinf-fin, append-assoc, toinfto-append-add, toinf-inf,
toinfto-append-addprovedall 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,
swap-to-from-appprovedall 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,
to-append-addprovedall subs proved to-zero, to-to-eq, size-to, size-to-02, append-assoc, to-fin, append-le-to, append-gr-to,
append-from-ge-02provedall subs proved size-inf, append-assoc, append-from-size-01, size-fin, from-zero, append-from-gr-02,
swap-inf-to-fromprovedall subs proved swap-inf-from-to,
toinf-empty3provedall subs proved to-empty3, fin-empty, toinf-add, toinf-inf,
to-empty3provedall subs proved size-succ, to-empty2,
append-toinf-lsprovedall subs proved toinf-fin, append-le-to, append-assoc, appendend-equal, toinf-inf,
swap-to-fromprovedall subs proved swap-from-to,
append-gr-toprovedall subs proved size-inf, to-inf, append-inf, append-assoc, append-to-gr-01, size-fin,
append-from-gr-02provedall subs proved size-inf, from-inf, append-inf, append-assoc, append-from-gr-01, size-fin,
swap-inf-from-toprovedall subs proved to-inf, from-inf, size-inf, swap-from-to,
leq-symmprovedall subs proved leq-symm-2,
to-attachprovedall subs proved append-assoc, append-to-size-01, to-succ-cons, append-finfin, to-zero-l, to-fin,
toinf-emptyprovedall subs proved to-empty, fin-empty, toinf-inf, empty, to-zero, toinf-fin,
append-to-addsize-01provedall subs proved to-zero, append-assoc, append-to-size-01, append-to-gr-01,
toinf-empty2provedall subs proved to-empty2, fin-empty, size-empty, toinf-inf, empty, to-zero, toinf-fin,
extensionality-toprovedall subs proved to-unwind-end, size-succ, extensionality,
appinf-to-ge-01provedall subs proved append-assoc, fin-finlen-tolen, appinf-to-split, appinf-to-ge,
append-from-ge-01provedall subs proved from-zero, append-assoc, append-from-size-01, append-from-gr-01,
leq-prefixprovedall subs proved finlen-tolen, append-le-to, size-empty-equiv, append-assoc, size-append, appendend-equal, prefix-def,
to-empty4provedall subs proved size-empty-equiv, to-empty2,
append-le-toprovedall subs proved to-inf, append-inf, append-assoc, append-to-le-01, size-fin, to-fin,
append-from-gr-01provedall subs proved append-assoc, append-from-addsize-01,
appinf-to-geprovedall subs proved to-empty-inf, fin-finlen-tolen, appinf-to-split,
swap-from-toprovedall subs proved from-to-exchange,
to-unwind-endprovedall 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,
append-from-size-01provedall subs proved from-zero, append-from-addsize-01,
append-to-gr-01provedall subs proved to-zero, cons-to-num, append-finfin, append-assoc, empty-append, empty,
to-empty2provedall subs proved to-empty-inf, to-inf, to-empty-fin2, size-fin, to-fin, to-zero,
to-emptyprovedall subs proved to-empty-inf, to-inf, to-empty-fin, size-fin, to-fin, to-zero,
append-to-size-01provedall subs proved fin-finlen-tolen, append-to-le-01,
leq-symm-2provedall subs proved append-assoc, prefixself-equal, appendend-equal, prefix-def,
toone-oneprovedall subs proved single-to-one, to-fin, append-assoc, append-empty, toone-cons,
toinf-empty-infprovedall subs proved to-empty-inf, fin-empty, fun-nonempty, toinf-inf, empty, to-zero-nf, to-inf, toinf-fin,
from-infto-exchangeprovedall subs proved from-to-exchange, toinf-fin, from-fin, toinf-add, toinf-inf,
append-from-le-01provedall subs proved from-succ-cons-l-lem, from-succ-cons, append-split-fin, append-finfin, append-assoc, empty-append, empty, from-zero-l, from-zero,
append-from-addsize-01provedall subs proved from-succ-cons, append-finfin, append-assoc, empty-append, empty,
append-to-le-01provedall subs proved to-succ-cons-l-lem, to-succ-cons, append-finfin, to-zero-l, to-zero, append-assoc, empty-append, empty,
prefixself-equalprovedall subs proved append-assoc, append-empty-01, empty-append, appendend-equal, prefix-def,
toone-consprovedall subs proved get-cons-zero, toone-equal, fin-empty, append-empty-01, append-assoc, toone-cons-fin, to-appfin,
from-to-exchangeprovedall subs proved append-assoc, size-fin, size-append, cons-append, from-succ-cons, from-succ-cons-l-lem, to-succ-cons, size-empty, elim-hd-tl, from-zero, from-zero-l,
cons-to-numprovedall subs proved append-assoc, to-succ-cons,
to-empty-finprovedall subs proved elim-fromto-fin, to-zero-l,
to-empty-infprovedall subs proved elim-fromto-inf, to-zero-nf,
from-append-toinffromprovedall subs proved from-append-tofrom, eq-stream-to-list-2-1, toinf-add, toinf-fin, append-assoc, to-plus-from-simp, toinf-inf,
cons-from-addnumprovedall subs proved append-assoc, from-succ-cons,
hd-appendprovedall subs proved append-assoc, hd-lem, cons-append, elim-hd-tl,
get-cons-numprovedall subs proved append-assoc, get-cons-succ,
to-unwind-beginprovedall subs proved append-assoc, get-cons-zero, cons-append, to-succ-cons, size-empty, elim-hd-tl,
leq-reflprovedall subs proved append-assoc, appendend-equal, prefix-def,
to-plus-fromprovedall subs proved append-assoc, to-plus-from-simp,
cons-from-numprovedall subs proved append-assoc, from-succ-cons,
to-plus-from-fin-simpprovedall subs proved elim-fromto-fin,
cons-to-addnumprovedall subs proved append-assoc, to-succ-cons,
hd-selzeroprovedall subs proved append-assoc, get-cons-zero, cons-append, elim-hd-tl,
expand-consprovedall subs proved one-inf, fun-nonempty, append-finfin, fin-empty,
elim-fromto-infprovedall subs proved append-fininf, size-fin, from-inf, to-inf, size-inf, elim-fromto,
elim-fromto-finprovedall subs proved to-plus-from-fin, append-from-size, append-to-size, length-to, elim-fromto,
get-cons-zeroprovedall subs proved sel-inf, one-inf, append-assoc, get-append2-fin,
get-cons-succprovedall subs proved one-inf, sel-inf, sel-fin, append-assoc, get-append2-fin,
to-succ-consprovedall subs proved to-succ-nf, one-inf, to-inf, to-fin, append-assoc, to-succ-cons-l-lem, to-appfin,
appendend-equalprovedall subs proved size-fin, size-inf, append-assoc, append-cancel-l-02,
elim-hd-tlprovedall 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-simpprovedall subs proved elim-fromto,
from-succ-consprovedall subs proved get-from-inf, from-nf, from-inf, one-inf, from-fin, append-assoc, from-succ-cons-l-lem, from-appfin,
to-is-prefixprovedall subs proved append-assoc, leq-append-right, size-append, elim-fromto,
from-succprovedall 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,
appfin-sel-01provedall subs proved eq-stream-to-list-3-1, append-assoc, neq-fin-inf-03,
from-cons-oneprovedall subs proved from-nf, from-inf, one-inf, from-cons-one-fin, from-fin, append-finfin,
eq-stream-to-list-3-1provedall subs proved eq-stream-to-list-2-1, append-assoc, append-split-fin, append-finfin,
append-cancel-l-02provedall subs proved neq-fin-inf-01, fun-nonempty, append-inf, append-assoc, append-empty, empty, eq-stream-to-list-2-1, fin-empty,
elim-fromtoprovedall 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-infprovedall subs proved append-assoc, append-split-fin, cons-append, intrace-expand,
cons-eq-01provedall subs proved neq-fin-inf-01, fin-empty, eq-stream-to-list-2-1, append-assoc, append-empty,
fin-neq-infprovedall subs proved append-assoc, neq-fin-inf-01, cons-append,
cons-eq-infprovedall subs proved append-fininf, append-assoc, neq-fin-inf-03, cons-append,
appfin-selprovedall subs proved eq-stream-to-list-2-1, append-assoc, neq-fin-inf-03,
append-cancel-lprovedall subs proved append-assoc, append-split-fin,
cons-appendprovedall subs proved append-fininf, cons-inf, append-assoc, append-split-fin, cons-fin, append-finfin,
eq-stream-to-list-2-1provedall subs proved append-assoc, append-split-fin, append-finfin,
leq-append-bothprovedall subs proved append-assoc, append-split-fin, leq-append-right, prefix-def,
append-cut1provedall subs proved append-inf, size-inf, size-fin, append-assoc, append-split-fin,
constrrewprovedall subs proved append-assoc, append-split-fin, append-finfin,
appinf-selfun-01provedall subs proved append-assoc, append-split-fin, appinf-selfun, append-fininf,
append-split-finprovedall subs proved size-fin, append-split,
append-splitprovedall 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,
toinf-to-eq-infprovedall subs proved toinf-to-eq, size-inf,
toinf-to-eqprovedall subs proved toinf-fin, to-to-eq, to-fin, toinf-inf,
cons-eqprovedall 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-leqprovedall subs proved append-assoc, append-empty-01, prefix-def, leq-empty,
fin-to-to-lsprovedall subs proved to-fin, size-fin, to-to-ls,
fin-to-to-eqprovedall subs proved to-fin, size-fin, to-to-eq,
toinf-to-lsprovedall subs proved to-to-ls, to-fin, toinf-fin, toinf-inf,
cons-emptyprovedall subs proved append-assoc, fin-empty, append-empty-01,
toinf-to-leq-infprovedall subs proved to-inf, toinf-to-leq, size-inf,
toinf-to-leqprovedall subs proved to-to-leq, to-fin, toinf-fin, toinf-inf,
finlen-tolenprovedall subs proved size-inf, size-fin, finlen-tolen-02,
to-to-eqprovedall subs proved to-to-leq,
to-to-lsprovedall subs proved to-to-leq,
neq-fin-inf-02provedall subs proved neq-fin-inf-03, append-fininf, append-assoc, append-inf,
append-empty-01provedall subs proved append-inf, fun-nonempty, append-fininf, empty, append-finfin, fin-empty, append-assoc, append-empty,
size-inf-toinfprovedall subs proved size-toinf, size-inf,
from-append-addprovedall 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,
append-notsmallersize1provedall subs proved append-assoc, size-append,
appinf-one2-get-succprovedall subs proved append-assoc, appinf-one-get-succ, append-fininf,
tl-oneprovedall subs proved empty, append-assoc, append-empty, tl-fin-lem,
appinf-one2-get-succ2provedall subs proved append-assoc, appinf-one-get-succ2, append-fininf,
append-to-addsizeprovedall subs proved to-zero-l, append-to-size, append-to-gr,
prefix-notsmallersizeprovedall subs proved append-assoc, size-append, prefix-def,
append-eq-infprovedall subs proved append-assoc, append-inf, neq-fin-inf-03,
appinf-one2-get-zeroprovedall subs proved append-assoc, appinf-one-get-zero, append-fininf,
contractinf-tlprovedall subs proved sel-fin, get-append-notls, get-append-ls, sel-inf, append-assoc, size-inf, size-fin, size-append, extensionality, tl-inf,
append-notsmallersize2provedall subs proved append-assoc, size-append,
get-fintoinfprovedall subs proved sel-fin, get-toinf, size-fin,
appinf-one2-to-succprovedall subs proved append-assoc, appinf-one-to-succ, append-fininf,
contractinf-from1provedall subs proved sel-fin, get-from-inf, get-append-notls, get-append-ls, sel-inf, append-assoc, size-inf, size-fin, size-append, extensionality,
fin-to-to-leqprovedall subs proved to-fin, size-fin, to-to-leq,
get-inftoinfprovedall subs proved sel-inf, get-toinf, size-inf,
hd-oneprovedall subs proved append-assoc, append-empty, empty, hd-fin-lem,
appinf-one2-to-succ2provedall subs proved append-assoc, appinf-one-to-succ2, append-fininf,
appinf-one-to-succ2provedall subs proved append-assoc, appinf-to-split,
appinf-one-to-succprovedall subs proved to-zero-nf, append-assoc, single-to-one, appinf-to-split,
get-toinfprovedall subs proved get-to, sel-fin, toinf-fin, toinf-inf,
get-append-lsprovedall subs proved append-inf, sel-inf, append-fininf, append-assoc, get-append2-fin, size-fin, sel-fin,
get-append-notlsprovedall subs proved size-inf, append-inf, append-fininf, sel-inf, sel-fin, append-assoc, get-append2-fin, size-fin,
appinf-one-get-zeroprovedall subs proved append-assoc, appinf-get-split,
finlen-tolen-02provedall subs proved size-inf, fin-finlen-tolen, to-fin, size-fin,
to-to-leqprovedall 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-emptyprovedall subs proved append-assoc, empty-append, prefix-def,
append-to-sizeprovedall subs proved fin-finlen-tolen, append-to-le,
append-from-sizeprovedall subs proved from-zero-l, append-from-addsize,
neq-fin-inf-03provedall subs proved append-finfin, append-assoc, append-inf,
appinf-one-get-succ2provedall subs proved append-assoc, appinf-get-split,
tl-lemprovedall subs proved tl-inf, append-fininf, append-assoc, tl-fin-lem,
appinf-one-get-succprovedall subs proved append-assoc, appinf-get-split,
hd-lemprovedall subs proved hd-inf, append-fininf, append-assoc, hd-fin-lem,
size-appendprovedall subs proved append-assoc, append-inf, size-inf, append-fininf, append-finfin, size-fin,
size-toinfprovedall subs proved size-to, size-to-02, toinf-fin, toinf-inf,
append-emptyprovedall subs proved append-assoc, append-inf, append-finfin, empty,
neq-fin-inf-01provedall subs proved append-assoc, append-inf, append-fininf,
from-append-tofromprovedall subs proved get-from, get-to, size-inf, from-inf, size-fin, length-from, from-fin, size-to,
ton-fromnprovedall subs proved ton-fromn-inf, to-inf, ton-fromn-fin, size-fin, to-fin,
appinf-to-leprovedall subs proved appinf-to-split,
get-from-zeroprovedall subs proved get-from,
lslen-fromnotemptyprovedall subs proved fun-nonempty, from-inf, lslen-fromnotempty-list, size-fin, fin-empty, from-fin,
to-to-eq-infprovedall subs proved to-to-leq-inf,
toinflenprovedall subs proved toinf-inf, size-inf, fin-finlen-tolen, to-fin, toinf-fin, size-fin,
to-from-01provedall subs proved ton-fromn-inf, to-inf, from-succ-cons-l-lem, to-succ-cons-l-lem, from-zero-l, to-zero-l, size-fin, to-fin,
leq-append-leftprovedall subs proved append-assoc, leq-append-right, prefix-def,
tl-fin-1provedall subs proved append-assoc, tl-fin-lem, append-finfin,
leq-transprovedall subs proved append-assoc, prefix-def,
to-plus-from-infprovedall subs proved append-assoc, to-plus-from-inf-simp,
append-from-addsizeprovedall subs proved from-all, append-from-le, from-zero-l, append-from-gt,
to-to-leq-infprovedall subs proved to-unwind-end-fin, size-inf-to, append-to-le, to-unwind-end-inf, to-zero-nf, to-zero-l,
lslen-fromnotempty-listprovedall subs proved length-from,
to-empty-fin2provedall subs proved length-to, to-zero-l,
appinf-to-splitprovedall subs proved get-finto, length-to, append-fininf, get-infto, size-inf-to,
fin-finlen-tolenprovedall subs proved to-all,
ton-fromn-finprovedall subs proved length-to, length-from,
ton-fromn-infprovedall subs proved size-inf-to, length-from,
fin-size-fromprovedall subs proved size-fin, length-from, from-fin,
less-size-fromprovedall subs proved size-inf, from-inf, size-fin, length-from, from-fin,
size-to-02provedall subs proved size-inf-to, to-inf, inf-size-to, to-fin, size-fin,
size-toprovedall subs proved size-inf-to, to-inf, length-to, size-fin, to-fin,
get-fromprovedall subs proved sel-inf, get-from-inf, from-inf, sel-fin, get-from-01, size-fin, from-fin,
get-toprovedall subs proved sel-inf, get-infto, to-inf, sel-fin, get-finto, size-fin, to-fin,
append-assocprovedall subs proved append-inf, append-fininf, eq-stream-to-list-3-3, append-finfin,
size-from-lessprovedall subs proved size-inf, from-inf, size-fin, length-from, from-fin,
size-fromprovedall subs proved size-inf, from-inf, size-fin, length-from, from-fin,
from-cons-one-finprovedall subs proved from-zero-l, from-succ-cons-l-lem,
append-from-gtprovedall subs proved from-succ-cons-l-lem,
append-from-leprovedall subs proved from-succ-cons-l-lem, from-zero-l,
from-allprovedall subs proved from-succ-cons-l-lem, from-zero-l,
size-empty-equivprovedall subs proved size-inf, fin-empty, size-fin, size-empty,
get-fintoprovedall subs proved to-succ-cons-l-lem, to-zero-l,
to-unwind-end-infprovedall subs proved to-succ-nf, to-zero-nf, to-inf-one,
append-to-leprovedall subs proved to-succ-cons-l-lem, to-zero-l,
toone-equalprovedall subs proved to-inf-one, to-inf, sel-inf, toone-cons-fin, fin-empty, sel-fin, to-fin,
to-unwind-end-finprovedall subs proved to-zero-l, to-succ-cons-l-lem,
eq-stream-to-list-3-3provedall subs proved eq-stream-to-list-2-2, append-finfin,
to-allprovedall subs proved to-succ-cons-l-lem, to-zero-l,
append-to-grprovedall subs proved to-succ-cons-l-lem,
to-plus-from-finprovedall subs proved from-succ-cons-l-lem, to-succ-cons-l-lem, from-zero-l, to-zero-l,
to-plus-from-inf-simpprovedall subs proved get-from-inf, size-inf-to, get-infto, append-fininf,
inf-size-toprovedall subs proved size-inf-to, size-fin,
length-toprovedall subs proved to-succ-cons-l-lem, to-zero-l,
single-to-oneprovedall subs proved to-zero-l, to-succ-cons-l-lem,
get-from-01provedall subs proved from-succ-cons-l-lem, from-zero-l,
length-fromprovedall subs proved from-succ-cons-l-lem, from-zero-l,
from-zeroprovedall subs proved from-nf-zero, from-inf, from-zero-l, from-fin,
get-append3-finprovedall subs proved get-append2-fin, append-finfin,
to-unwind-begin-finprovedall subs proved to-succ-cons-l-lem,
to-inf-twoprovedall subs proved get-infto, size-inf-to,
from-fromprovedall subs proved get-from-inf, from-nf, size-inf, from-inf, from-succ-cons-l-lem, from-zero-l, size-fin, from-fin,
from-from-infprovedall subs proved get-from-inf,
zero-lenprovedall subs proved size-inf, fun-nonempty, size-fin, fin-empty,
intrace-expandprovedall subs proved cons-inf,
from-nf-zeroprovedall subs proved from-nf,
appinf-selfunprovedall subs proved append-fininf,
hd-fin-lemprovedall subs proved hd-fin, append-finfin,
toone-cons-finprovedall subs proved to-zero-l, to-succ-cons-l,
to-appfinprovedall subs proved to-fin, append-finfin,
eq-stream-to-list-2-2provedall subs proved append-finfin,
leq-append-rightprovedall subs proved prefix-def,
get-inftoprovedall subs proved to-succ-nf, to-zero-nf,
size-emptyprovedall subs proved size-fin, empty,
size-succprovedall subs proved size-inf, size-fin,
tl-fin-lemprovedall subs proved tl-fin, append-finfin,
get-append2-finprovedall subs proved sel-fin, append-finfin,
to-inf-oneprovedall subs proved to-zero-nf, to-succ-nf,
to-zeroprovedall subs proved to-zero-nf, to-inf, to-zero-l, to-fin,
appinf-get-splitprovedall subs proved append-fininf,
to-succ-cons-l-lemprovedall subs proved to-succ-cons-l,
extensionalityprovedall subs proved sel-inf, size-inf, sel-fin, size-fin,
get-from-infprovedall subs proved from-nf,
from-appfinprovedall subs proved from-fin, append-finfin,
size-inf-toprovedall subs proved to-succ-nf, to-zero-nf,
fin-emptyprovedall subs proved empty,
fun-nonemptyprovedall subs proved empty,
toinf-addprovedall subs proved toinf-fin,
empty-appendprovedall subs proved append-fininf, append-finfin, empty,
from-succ-cons-l-lemprovedall subs proved from-succ-cons-l,
get-from-inf-zeroprovedall subs proved from-nf,
to-succ3-nfprovedall subs proved to-succ-nf,
eq-stream-to-list-3-2provedall subs proved append-finfin,
appinf-get-ge-01provedall subs proved append-fininf,
extract-emptyprovedall subs proved empty,
inf-size-fromprovedall subs proved size-inf, from-inf, size-fin,
inf-not-toinf-exceptinfprovedall subs proved toinf-fin, toinf-inf,
size-from-infprovedall subs proved size-inf, from-inf,
to-succ2-nfprovedall subs proved to-succ-nf,
appinf-get-geprovedall subs proved append-fininf,
appinf-get-leprovedall subs proved append-fininf,
tl-inf-1provedall subs proved tl-inf, cons-inf,
cons-finaxiom
from-succ-cons-laxiom
cons-infaxiom
tl-finaxiom
hd-infaxiom
tl-infaxiom
prefix-defaxiom
to-zero-nfaxiom
to-succ-cons-laxiom
to-zero-laxiom
hd-finaxiom
to-succ-nfaxiom
from-nfaxiom
to-finaxiom
to-infaxiom
from-infaxiom
sel-infaxiom
append-fininfaxiom
size-finaxiom
from-finaxiom
sel-finaxiom
size-infaxiom
append-infaxiom
toinf-infaxiom
toinf-finaxiom
from-zero-laxiom
emptyaxiom
append-finfinaxiom