PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: lang eq imp quo eq 1 1 1 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
9. z: Alph* = Alph*
10. x: Alph*
11. y: Alph*
12. z:Alph*. LangOf(A1)(z @ x) LangOf(A1)(z @ y)

z:Alph*. LangOf(A2)(z @ x) LangOf(A2)(z @ y)
By: SimilarTo -1
Generated subgoals:

112. z1: Alph*
13. LangOf(A1)(z1 @ x) LangOf(A1)(z1 @ y)
LangOf(A2)(z1 @ x) LangOf(A2)(z1 @ y)
212. z1: Alph*
13. (LangOf(A1)(z1 @ x)) (LangOf(A1)(z1 @ y))
(LangOf(A2)(z1 @ x)) (LangOf(A2)(z1 @ y))

About:
alllistapplyuniverseequalimplies