PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: min is unique 1 1 1 1 1
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

f:(St(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))). Bij(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); f) & (s:St, a:Alph. f(Auto(s,a)) = A(l.Auto(l))(f(s),a) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) & f(InitialState(Auto)) = InitialState(A(l.Auto(l))) x,y:Alph*//(x LangOf(Auto)-induced Equiv y) & (s:St. FinalState(Auto)(s) = FinalState(A(l.Auto(l)))(f(s)))
By:
Witness f
THEN
Reduce 0
Generated subgoals:

1 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)))
210. f1: St(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
11. s: St
12. a: Alph
a.f1(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
310. f1: St(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
nil x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
410. f1: St(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
11. s: St
Auto(f1(s))

About:
existsfunctionquotientlistandallequal
applylambdabooluniverseconsnilmember