PrintForm
Definitions
automata
4
Sections
AutomataTheory
Doc
At:
homo
init
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.
g:
(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
6.
c:
St
Alph*
7.
q:St. (Result(Auto)c(q)) = q
(Result(Auto)c(InitialState(Auto))) = (Result(Auto)nil)
By:
RWH (HypC 7) 0
Generated subgoal:
1
InitialState(Auto) = (Result(Auto)nil)
About:
InitialState(Auto) = (Result(Auto)nil)
Alph*
q:St. (Result(Auto)c(q)) = q (Result(Auto)c(InitialState(Auto))) = (Result(Auto)nil) InitialState(Auto) = (Result(Auto)nil)
