Thms nfa 1 Sections AutomataTheory Doc

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

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