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

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