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