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

Theorem base summary for Specification stream

append-assoc(19,10)append-inf(0,0)cons-to-num(3,0)fin-to(1,1)from-succ-cons-l-lem(2,2)hd-fin-lem(3,3)neq-fin-inf-01(3,2)swap-inf-from-to(1,1)to-inf(0,0)toinf-add(2,2)
append-cancel-l(10,7)append-notsmallersize1(1,0)constrrew(1,0)fin-toinf(1,0)from-to-exchange(5,3)hd-inf(0,0)neq-fin-inf-02(4,3)swap-inf-to-from(4,1)to-inf-one(2,1)toinf-empty(2,0)
append-cancel-l-02(6,3)append-notsmallersize2(1,0)contractinf-from1(5,2)finlen-tolen(2,1)from-zero(1,1)hd-lem(2,2)neq-fin-inf-03(5,3)swap-inf-to-from-app(4,1)to-plus-from(1,0)toinf-empty-inf(2,0)
append-cancel-r-01(1,0)append-split(21,13)contractinf-tl(6,2)finp-append-01(1,0)from-zero-l(0,0)hd-one(1,1)nlslen-lslensn-eqlensn(1,0)swap-to-from(4,1)to-plus-from-fin(6,2)toinf-empty2(2,0)
append-cancel-r-02(2,1)append-to-addsize(1,1)elim-fromto(16,8)finp-append-02(1,1)fun-nonempty(1,1)inf-not-to(2,1)notfin-sizeinf(1,0)swap-to-from-app(44,17)to-plus-from-fin-simp(1,1)toinf-empty3(2,1)
append-cancel-r-04(1,1)append-to-addsize-01(1,1)elim-fromto-fin(1,1)finp-empty(1,1)get-append-ls(5,3)inf-not-toinf-exceptinf(2,1)one-inf(2,1)tl-fin(0,0)to-plus-from-inf(3,2)toinf-fin(0,0)
append-cut1(1,1)append-to-gr(6,1)elim-fromto-inf(3,2)finp-infto(1,0)get-append-notls(8,3)inf-size-from(2,1)prefix-def(0,0)tl-fin-1(1,1)to-plus-from-inf-simp(5,1)toinf-inf(0,0)
append-empty(3,3)append-to-gr-01(10,2)elim-hd-tl(10,3)finp-to(1,0)get-append2-fin(2,2)inf-size-to(1,0)sel-fin(0,0)tl-fin-lem(3,3)to-plus-from-simp(2,1)toinf-to-eq(2,0)
append-empty-01(9,6)append-to-le(6,2)empty(0,0)from-all(1,1)get-append3-fin(2,2)intrace-expand(5,1)sel-inf(0,0)tl-inf(0,0)to-succ-cons(6,3)toinf-to-eq-inf(1,0)
append-eq-inf(1,0)append-to-le-01(6,2)empty-append(5,5)from-append-add(33,16)get-cons-num(2,1)length-from(8,2)single-to-one(1,1)tl-inf-1(1,1)to-succ-cons-l(0,0)toinf-to-leq(2,1)
append-extract-list(5,0)append-to-ls(2,0)empty-leq(2,1)from-append-tofrom(14,6)get-cons-succ(3,2)length-to(6,2)size-append(7,5)tl-lem(2,2)to-succ-cons-l-lem(2,2)toinf-to-leq-inf(1,0)
append-extract-list-2(1,0)append-to-size(1,1)eq-stream-to-list-2-1(3,2)from-append-toinffrom(4,2)get-cons-zero(2,2)leq-append-both(5,2)size-empty(2,2)tl-one(1,1)to-succ-nf(0,0)toinf-to-ls(2,1)
append-finfin(0,0)append-to-size-01(1,1)eq-stream-to-list-2-2(3,3)from-appfin(2,2)get-finto(10,3)leq-append-left(2,1)size-empty-equiv(2,1)to-all(1,1)to-to-eq(2,1)toinflen(2,0)
append-fininf(0,0)append-toinf-ls(2,1)eq-stream-to-list-3-1(3,2)from-cons-one(7,6)get-fintoinf(1,0)leq-append-right(2,1)size-fin(0,0)to-append-add(4,2)to-to-eq-inf(1,1)toinfto-append-add(1,0)
append-from-addsize(3,2)appendend-equal(1,0)eq-stream-to-list-3-2(4,4)from-cons-one-fin(1,1)get-from(2,1)leq-empty(1,1)size-from-inf(1,0)to-appfin(2,2)to-to-leq(19,8)toinftoinf-append-add(4,2)
append-from-addsize-01(3,1)cons-append(5,5)eq-stream-to-list-3-3(3,3)from-fin(0,0)get-from-01(6,2)leq-prefix(4,1)size-from-less(2,0)to-attach(1,0)to-to-leq-inf(17,7)ton-fromn(4,2)
append-from-ge-01(1,1)cons-empty(1,0)expand-cons(13,4)from-from(11,5)get-from-inf(1,1)leq-refl(1,1)size-inf(0,0)to-empty(2,1)to-to-ls(2,1)ton-fromn-fin(2,1)
append-from-ge-02(3,2)cons-eq(11,9)extensionality(13,5)from-from-inf(1,1)get-from-inf-zero(1,1)leq-symm(1,0)size-inf-to(5,2)to-empty-fin(2,1)to-unwind-begin(2,1)ton-fromn-inf(1,1)
append-from-gr-01(2,0)cons-eq-inf(8,2)extensionality-to(9,5)from-inf(0,0)get-from-zero(2,1)leq-symm-2(4,2)size-inf-toinf(1,0)to-empty-fin2(2,1)to-unwind-begin-fin(2,0)toone-cons(1,1)
append-from-gr-02(1,1)cons-extract-list(5,2)extract-empty(2,2)from-infto-exchange(4,2)get-infto(9,3)leq-trans(7,4)size-succ(1,1)to-empty-inf(2,1)to-unwind-end(17,9)toone-cons-fin(1,1)
append-from-gt(6,1)cons-fin(0,0)fin-empty(2,2)from-nf(0,0)get-inftoinf(1,0)less-size-from(2,1)size-to(1,1)to-empty2(2,1)to-unwind-end-fin(6,2)toone-equal(4,0)
append-from-le(6,2)cons-from-addnum(3,0)fin-finlen-tolen(1,0)from-nf-zero(1,1)get-to(2,1)lslen-fromnotempty(2,0)size-to-02(2,1)to-empty3(2,1)to-unwind-end-inf(6,3)toone-one(1,1)
append-from-le-01(6,2)cons-from-num(3,0)fin-neq-inf(1,0)from-succ(17,5)get-to-02(2,1)lslen-fromnotempty-list(2,1)size-toinf(2,0)to-empty4(2,1)to-zero(1,1)zero-len(1,1)
append-from-size(1,1)cons-inf(0,0)fin-size-from(1,0)from-succ-cons(4,4)get-toinf(2,1)modify-fin(0,0)stream-empty(1,0)to-fin(0,0)to-zero-l(0,0)
append-from-size-01(1,1)cons-to-addnum(3,0)fin-size-from2(1,0)from-succ-cons-l(0,0)hd-fin(0,0)modify-inf(0,0)swap-from-to(21,11)to-from-01(8,3)to-zero-nf(0,0)