Nuprl - Pf min_auto

Alph,St:Type, Auto:Automata(Alph;St). LangOf(Auto) = LangOf(MinAuto(Auto))

By: Unfold `auto_lang` 0 THEN Unfold `lang_eq` 0 THEN Unfold `min_auto` 0 THEN UnivCD THEN Reduce 0

Generated subgoal:

1 1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. l: Alph*
Auto(l) A(l.Auto(l))(l)

About: