PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
quo
list
accept
1
1
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
5.
l1:
Alph*
6.
l2:
Alph*
7.
l1 LangOf(Auto)-induced Equiv l2
Auto(l1)
= Auto(l2)
By:
Unfold `lang_rel` 7
THEN
Reduce 7
THEN
Witness7 nil
THEN
Reduce 7
Generated subgoal:
1
7.
LangOf(Auto)(l1)
LangOf(Auto)(l2)
Auto(l1)
= Auto(l2)
About:
LangOf(Auto)(l2)
Auto(l1)
= Auto(l2) Auto(l1) = Auto(l2) LangOf(Auto)(l2) Auto(l1) = Auto(l2)
