Nuprl - Pf min_auto_con 1 1 1 3 1

PrintForm Definitions automata 5 Sections AutomataTheory Doc

1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph) & Fin(St)
5. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
6. s: x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
7. h: Alph*Alph*
8. x,y:Alph*. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y) h(x) = h(y)
9. x:Alph*. x = h(x) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)

l:Alph*. (Result(MinAuto(Auto))l) = s

By: Witness h(s)

Generated subgoals:

1 h(s) Alph*

2 (Result(MinAuto(Auto))h(s)) = s

3 10. l: Alph*
(Result(MinAuto(Auto))l) = s Prop

About:

1	`h(s) Alph*`
2	`(Result(MinAuto(Auto))h(s)) = s`
3	10. `l:` `Alph*` `(Result(MinAuto(Auto))l) = s Prop`