PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
homo
is
surj
1
1
2
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
c:
St
Alph*
5.
q:St. (Result(Auto)c(q)) = q
6.
Fin(Alph)
7.
Fin(St)
8.
EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
9.
x:
Alph*
10.
y:
Alph*
Dec(x (
x,y. x = y
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) y)
By:
Reduce 0
Generated subgoal:
1
Dec(x = y
x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
About:
Dec(x = y 
x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
Alph*
q:St. (Result(Auto)c(q)) = q Dec(x (
x,y. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) y) Dec(x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
