PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd comp init thm 6
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)

2of(hd(rev([ < I(NDA),nil > ]))) = nil Alph*
By:
RecUnfold `reverse` 0
THEN
Reduce 0
Generated subgoals:

None

About:
equallistconspairniluniverse