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