Thms
nfa
1
Sections
AutomataTheory
Doc
length
Def
(rec) ||as|| == Case of as : null
0 ; a.as'
||as'||+1
Thm*
l:A*. ||l||
Thm*
||nil||