Nuprl - Pf reach_lemma 1 1 2 1

PrintForm Definitions det automata Sections AutomataTheory Doc

1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. nn:
5. f: nnAlph
6. g: Alphnn
7. Fin(S.car)
8. InvFuns(nn; Alph; f; g)
9. s: S.car
10. si = s False

w:Alph*. (S:wsi) = s

By: InstConcl [nil] THEN RecUnfold `maction` 0 THEN Reduce 0 THEN Analyze 10

Generated subgoals:

None

About: