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