Thms nfa 1 Sections AutomataTheory Doc

list_p Def T List == {l:(T*)| ||l|| > 0}

Thm* (T List) Type

length Def (rec) ||as|| == Case of as : null 0 ; a.as' ||as'||+1

Thm* l:A*. ||l||

Thm* ||nil||

gt Def i > j == j < i

Thm* i,j:. i > j Prop