PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
any
iso
min
auto
1
1
2
1
1
1
1
3
1
1
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.
Auto(l1)
Auto(l2)
Auto(l1)
= A(l2)
By:
FwdThru
Thm*
a,b:
. (a
b)
a = b [16]
Generated subgoal:
1
17.
Auto(l1)
= Auto(l2)
Auto(l1)
= A(l2)
About:
= Auto(l2)
Auto(l1) = A(l2)
A(
l.A(l)) 
Auto(l2) Auto(l1) = A(l2)
a,b:
. (a b) 
a = b
[16] = Auto(l2) Auto(l1) = A(l2)
