PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
any
ge
min
auto
1
1
2
2
1
2
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
S:
Type
5.
A:
Automata(Alph;S)
6.
Fin(Alph)
7.
Fin(St)
8.
LangOf(Auto) = LangOf(A)
9.
Con(A)
10.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
11.
EquivRel x,y:Alph*. x LangOf(A)-induced Equiv y
12.
A
A(
l.Auto(l)
)
13.
x,y:Alph*//(x LangOf(Auto)-induced Equiv y) = x,y:Alph*//(x LangOf(A)-induced Equiv y)
A
A(
l.Auto(l)
)
By:
RWH (HypC 13) 0 THENL [Auto;Auto;Auto;Id;Auto;Auto;Auto]
Generated subgoal:
1
A(
l.Auto(l)
) = A(
l.Auto(l)
)
Automata(Alph;x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
About:
A(
l.Auto(l)
) = A(l.Auto(l)) 
Automata(Alph;x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
A(l.Auto(l)) A A(l.Auto(l)) A(l.Auto(l)) = A(l.Auto(l)) Automata(Alph;x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
