PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd compute list wf 1 1 1
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. l: Alph*
5. q: St

NDA(nil)q Prop
By:
RecCaseSplit `nd_compute_list`
THEN
Analyze 6
THEN
Reduce 0
Generated subgoals:

None

About:
memberpropniluniverselist