PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd valcom wf 3
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. C: (StAlph*)*
5. ||C|| > 0
6. i:(||C||-1). ||2of(C[i])|| > 0
7. q: St

||rev(C)||1
By: Unhide
Generated subgoals:

None

About:
natural_numberuniverselistproductallsubtract