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