PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd valcom wf 1
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
8. i: (||C||-1)

||rev(2of(C[i]))||1
By: Unhide
Generated subgoal:

15. ||C|| > 0
6. i:(||C||-1). ||2of(C[i])|| > 0
7. q: St
8. i: (||C||-1)
||rev(2of(C[i]))||1

About:
natural_numberuniverselistproductallsubtract