PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
min
auto
wf
1
1
1
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.
LangOf(Auto)(l1)
LangOf(Auto)(l2)
Auto(l1)
= Auto(l2)
By:
Unfold `auto_lang` 7
THEN
Reduce 7
Generated subgoal:
1
7.
Auto(l1)
Auto(l2)
Auto(l1)
= Auto(l2)
About:
Auto(l2)
Auto(l1)
