Nuprl - Pf mn_12 1 2 2 1 2 1 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. Alph: Type
2. L: LangOver(Alph)
3. Fin(Alph)
4. St: Type
5. Auto: Automata(Alph;St)
6. Fin(St)
7. L = LangOf(Auto)
8. EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)

(l.Auto(l)) (x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)))

By: Analyze

Generated subgoals:

1 9. l: x,y:Alph*//((Result(Auto)x) = (Result(Auto)y))
Auto(l)

2 x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)) Type

About:

1	9. `l:` `x,y:Alph*//((Result(Auto)x) = (Result(Auto)y))` `Auto(l)`
2	`x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)) Type`