PrintForm
Definitions
automata
6
Sections
AutomataTheory
Doc
At:
auto3
1
minimization
1
Fin(x,y:
1*//(x LangOf(Auto3_1)-induced Equiv y))
By:
BackThru
Thm*
Auto:Automata(Alph;St). Fin(Alph) & Fin(St)
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
THEN
Analyze 0
THEN
BackThru
Thm*
n:
. Fin(
n)
Generated subgoals:
None
About:
Fin(x,y:
1*//(x LangOf(Auto3_1)-induced Equiv y))
Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) 
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
n:. Fin(n)