PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: any ge min auto 1 1 2 2 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. S: Type
5. A: Automata(Alph;S)
6. Fin(Alph)
7. Fin(St)
8. LangOf(Auto) = LangOf(A)
9. Con(A)
10. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
11. EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
12. A A(l.Auto(l))

x,y:Alph*//(x LangOf(Auto)-induced Equiv y) = x,y:Alph*//(x LangOf(A)-induced Equiv y)
By:
refine (make_primitive_rule RULE H x,y:A//E = u,v:B//F Type{i} BY quotientEquality r; s; w H x,y:A//E Type{i} H u,v:B//F Type{i} H A = B Type{i} H, w:(A = B Type{i}), r:A, s:A E[r,s/x,y] F[r,s/u,v] [make_variable_argument `x';make_variable_argument `y';make_variable_argument `z'])
THEN
Unfold `lang_rel` 0
THEN
Unfold `lang_rel` 16
THEN
Reduce 0
THEN
Reduce 16
THEN
Analyze 0
THEN
Unfold `lang_eq` 8
Generated subgoals:

18. l:Alph*. LangOf(Auto)(l) LangOf(A)(l)
9. Con(A)
10. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
11. EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
12. A A(l.Auto(l))
13. z: Alph* = Alph*
14. x: Alph*
15. y: Alph*
16. z:Alph*. LangOf(Auto)(z @ x) LangOf(Auto)(z @ y)
17. z1: Alph*
LangOf(A)(z1 @ x) LangOf(A)(z1 @ y)
28. l:Alph*. LangOf(Auto)(l) LangOf(A)(l)
9. Con(A)
10. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
11. EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
12. A A(l.Auto(l))
13. z: Alph* = Alph*
14. x: Alph*
15. y: Alph*
16. z:Alph*. LangOf(A)(z @ x) LangOf(A)(z @ y)
17. z1: Alph*
LangOf(Auto)(z1 @ x) LangOf(Auto)(z1 @ y)

About:
equaluniversequotientlistlambdaapply