PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
any
iso
min
auto
1
1
2
1
1
1
1
3
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
S:
Type
5.
A:
Automata(Alph;S)
6.
Fin(Alph)
7.
Fin(S)
8.
Con(A)
9.
S ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
10.
LangOf(Auto) = LangOf(A)
11.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
12.
EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
13.
A
A(
l.A(l)
)
14.
l1:
Alph*
15.
l2:
Alph*
16.
l1 LangOf(Auto)-induced Equiv l2
Auto(l1)
= A(l2)
By:
Unfold `lang_rel` 16
THEN
Reduce 16
THEN
Witness16 nil
THEN
Reduce 16
Generated subgoal:
1
16.
LangOf(Auto)(l1)
LangOf(Auto)(l2)
Auto(l1)
= A(l2)
About:
LangOf(Auto)(l2)
Auto(l1)
= A(l2)
A(
l.A(l)) Auto(l1) = A(l2) LangOf(Auto)(l2) Auto(l1) = A(l2)
