Thms exponent Sections AutomataTheory Doc

en Def (rec) en(l) == if null(l) 0 else hd(l)+en(tl(l))n fi

Thm* n:, l:n*. en(l)

tl Def tl(l) == ListInd(l;nil;h,t,v.t)

Thm* l:A*. tl(l) A*

hd Def hd(l) == ListInd(l;"?";h,t,v.h)

Thm* l:A*. (||l|| 1 ) hd(l) A

null Def null(as) == Case of as : null true ; a.as' false

Thm* as:T*. null(as)

Thm* null(nil)