Nuprl - Pf min_is_unique 1 1 1 1 1 1

PrintForm Definitions automata 5 Sections AutomataTheory Doc

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

Bij(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); f) & (s:St, a:Alph. f(Auto(s,a)) = a.f(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) & f(InitialState(Auto)) = nil x,y:Alph*//(x LangOf(Auto)-induced Equiv y) & (s:St. FinalState(Auto)(s) = Auto(f(s)))

By: Auto

Generated subgoals:

1 Bij(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); f)

2 10. s: St
11. a: Alph
f(Auto(s,a)) = a.f(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)

3 f(InitialState(Auto)) = nil x,y:Alph*//(x LangOf(Auto)-induced Equiv y)

4 10. s: St
FinalState(Auto)(s) = Auto(f(s))

About:

1	`Bij(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); f)`
2	10. `s:` `St` 11. `a:` `Alph` `f(Auto(s,a)) = a.f(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)`
3	`f(InitialState(Auto)) = nil x,y:Alph*//(x LangOf(Auto)-induced Equiv y)`
4	10. `s:` `St` `FinalState(Auto)(s) = Auto(f(s))`