PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd comp length wf 1 1
1. Alph: Type
2. St: Type
3. C: (StAlph*)*
4. ||C|| > 0
5. i:(||C||-1). ||2of(C[i])|| > 0

||C||
By: Unfold `nd_comp_length` 0
Generated subgoals:

None

About:
memberintuniverselistproductnatural_numberallsubtract