At: lang eq imp quo eq 1 1 1 2
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
9. z: Alph* = Alph*
10. x: Alph*
11. y: Alph*
12. x LangOf(A2)-induced Equiv y
x LangOf(A1)-induced Equiv y
By: {like the other branch }
Unfold `lang_rel` 0 THEN Reduce 0 THEN Unfold `lang_rel` -1 THEN Reduce -1 THEN SimilarTo -1
THENL
[SimilarTo -1;SimilarTo -1 THENP BackThru: 6 THENL [BackThru: 6;
Def of LangOver( < Alph > )]]
THENP
BackThru: 6
THENL
[BackThru: 6;Def of LangOver( < Alph > )]
Generated subgoals:None
About:
