PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd comp init thm 3
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. i: (||[ < I(NDA),nil > ]||-1)

2of([ < I(NDA),nil > ][(i+1)]) = rev(tl(rev(2of([ < I(NDA),nil > ][i])))) Alph*
By: Reduce 4
Generated subgoals:

None

About:
equallistaddnatural_numbercons
pairniluniversesubtract