Nuprl - Pf mn_31 1 1 1

1. Alph: Type
2. L: LangOver(Alph)
3. EquivRel x,y:Alph*. x L-induced Equiv y

Fin(Alph) Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l))) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))

By: UnivCD THENW (Auto THEN Fold `languages` 0)

Generated subgoal:

1 4. Fin(Alph)
5. Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l)))
St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto)

About: