[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 list-last

b(1,1)blastn-app-1(1,1)l-04(2,0)le-leq-one-empty-or-first-equal-last(2,0)mk-len(0,0)postfix(0,0)postfix-more-01(1,0)prefix-app-04(1,0)prefix-more(1,0)rev-disjoint-01(7,0)
b-01(2,0)blastn-len-0(2,1)l-05(1,0)lin(2,0)mk-one(1,0)postfix-app(2,1)postfix-one(4,3)prefix-app-05(1,0)prefix-nil(1,0)rev-dups(3,2)
b-02(1,0)bnotempty(2,1)l-06(2,0)lin-01(2,0)mk-one-01(2,0)postfix-app-01(1,0)postfix-one-less(1,0)prefix-app-size-eq(2,1)prefix-notin(1,0)rev-e(0,0)
bapp(2,0)btwo(1,1)l-in(2,0)lin-02(1,0)mk-plus(3,0)postfix-app-02(1,0)postfix-rec(4,2)prefix-attach(2,1)prefix-one(2,1)rev-empty(2,0)
bc(1,0)butlast-def(1,1)lapp(2,0)lthree(2,0)mk-rec(2,1)postfix-app-04(1,0)postfix-rec-right(10,6)prefix-butlast(2,1)prefix-one-01(5,3)rev-in(7,0)
bin(3,0)butlast-eq(2,1)lapp-01(1,1)mk-butlast(6,2)mk-rest(2,0)postfix-app-05(1,0)postfix-reflexivity(1,0)prefix-butlast-append(2,1)prefix-rec(2,0)rev-length(1,0)
bin-01(2,1)butlast-last(3,2)lapp-02(1,0)mk-butlast-01(6,2)mk-rest-01(2,0)postfix-app-06(1,0)postfix-rest(2,0)prefix-empty(1,0)prefix-rec-01(1,0)rev-mklist(5,3)
bin-02(2,1)butlast-last-01(1,0)lapp-03(1,0)mk-elem(0,0)mk-succ(11,4)postfix-empty(1,0)postfix-rest-01(2,0)prefix-empty-03(1,0)prefix-rec-02(1,0)rev-one(1,1)
bl(1,0)butlast-len(1,1)lapp-04(2,0)mk-empty(2,0)mk-two(6,2)postfix-empty-01(1,0)postfix-same(1,0)prefix-eq(2,1)prefix-rec-03(1,0)rev-r(0,0)
blapp(2,1)butlastN-base(0,0)lapp-05(2,0)mk-first(2,0)mk-two-01(1,1)postfix-empty-02(1,0)postfix-split-stronger(10,5)prefix-equality(1,0)prefix-same(1,0)rev-rest(6,0)
blapp-01(1,0)butlastN-rec(0,0)last-01(1,0)mk-first-01(2,0)mk-zero(1,1)postfix-empty-03(1,0)postfix-trans(5,3)prefix-ex(9,4)prefix-same-01(1,0)rev-rev-identity(1,0)
blast-first(6,1)consmklist-last(1,1)last-02(0,0)mk-in(2,0)mklist-append(1,0)postfix-in(1,0)postifx-app-03(1,0)prefix-in(2,1)prefix-self(1,0)rev-rewrite(1,0)
blastN-all(1,1)fillfirst-fill(0,0)last-def(1,1)mk-inj(4,2)mklist-last(1,0)postfix-in-01(1,0)postifx-split(2,1)prefix-in-01(2,1)prefix-size-eq(2,1)revert-equal(3,2)
blastN-all-01(1,0)fillfirst-longer(0,0)last-elim(1,0)mk-inj-01(10,3)mklist-one(1,1)postfix-in-02(1,0)prefix(0,0)prefix-in-02(1,0)prefix-split(2,1)revert-last(1,0)
blastN-len(12,5)l(1,1)last-ex(6,3)mk-last(3,0)mklist-rmdup(10,2)postfix-in-03(2,1)prefix-app(2,1)prefix-in-03(2,1)prefix-split-stronger(6,2)splitlasteq(1,0)
blastN-mklist(8,4)l-01(2,0)last-one(2,0)mk-last-01(6,2)mklist-rmdup-01(8,3)postfix-is-lessOrEqual(6,4)prefix-app-01(4,0)prefix-intro(2,1)prefix-trans(6,2)splitlasteq-01(1,0)
blastN-rec(2,0)l-02(1,0)lb(4,4)mk-last-01-01(2,1)mklist-split-intro(2,0)postfix-length(4,2)prefix-app-02(2,1)prefix-longer(1,0)rev-app(3,0)
blastN-rec-01(12,6)l-03(2,0)lb-01(1,0)mk-last-02(2,0)nodups-butlastn(23,8)postfix-more(4,2)prefix-app-03(2,1)prefix-longer-01(2,1)rev-disjoint(5,0)