PrintForm
Definitions
automata
6
Sections
AutomataTheory
Doc
At:
oddeven
minimization
1
1.
n:
Fin(x,y:
n*//(x LangOf(OddEven#n)-induced Equiv y))
By:
Inst
Thm*
Auto:Automata(Alph;St). Fin(Alph) & Fin(St)
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) [
n;
(2
n);OddEven#n]
THEN
BackThru
Thm*
n:
. Fin(
n)
Generated subgoals:
None
About:
Fin(x,y:n*//(x LangOf(OddEven#n)-induced Equiv y))
Auto:Automata(Alph;St).
Fin(Alph) & Fin(St) 
Fin(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
[n;(2
n);OddEven#n]
n:. Fin(n)