PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: lang eq imp quo eq 1 1
1. Alph: Type
2. S1: Type
3. S2: Type
4. A1: Automata(Alph;S1)
5. A2: Automata(Alph;S2)
6. LangOf(A1) = LangOf(A2)
7. EquivRel x,y:Alph*. x LangOf(A1)-induced Equiv y
8. EquivRel x,y:Alph*. x LangOf(A2)-induced Equiv y

x,y:Alph*//(x LangOf(A1)-induced Equiv y) = x,y:Alph*//(x LangOf(A2)-induced Equiv y)
By:
Refine 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] RuleArgs:[x:v ; y:v ; z:v]
THEN
Try (Complete Auto)
Generated subgoal:

19. z: Alph* = Alph*
10. x: Alph*
11. y: Alph*
(x LangOf(A1)-induced Equiv y) (x LangOf(A2)-induced Equiv y)

About:
equaluniversequotientlistaxiommember