automata
4
Sections
AutomataTheory
Doc
Def
|S|
|T| ==
f:(S
T). Surj(S; T; f)
Thm*
A1:Automata(Alph;S1), A2:Automata(Alph;S2). Con(A1) & Con(A2)
A1
A2
|S1|
|S2| refine_ge
A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) 
A1 
A2 |S1| 
|S2|
refine_ge
|T| == 
f:(S
T). Surj(S; T; f)
A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) A1 A2 |S1| |S2|
refine_ge