n:
.
k:, f:(k
(x,y:n*//(x LangOf(OddEven#n)-induced Equiv y))).
Bij(k; x,y:n*//(x LangOf(OddEven#n)-induced Equiv y); f)
oddeven_minimization
} == {k:
| i 
k < j }
Thm* n:.
k:, f:(k(x,y:n*//(x LangOf(OddEven#n)-induced Equiv y))).
Bij(k; x,y:n*//(x LangOf(OddEven#n)-induced Equiv y); f)
oddeven_minimization
Thm* n:. OddEven#n 
Automata(n;(2
n)) auto_oddeven_wf
Thm* n:, f:(n(x,y:2*//(x LangOf(Auto4)-induced Equiv y))).
Bij(n; x,y:2*//(x LangOf(Auto4)-induced Equiv y); f)
auto4_minimization
Thm* n:, f:(n(x,y:3*//(x LangOf(auto3_3())-induced Equiv y))).
Bij(n; x,y:3*//(x LangOf(auto3_3())-induced Equiv y); f)
auto3_3_minimization
Thm* n:, f:(n(x,y:2*//(x LangOf(auto3_23())-induced Equiv y))).
Bij(n; x,y:2*//(x LangOf(auto3_23())-induced Equiv y); f)
auto3_23_minimization
Thm* n:, f:(n(x,y:2*//(x LangOf(Auto3_2)-induced Equiv y))).
Bij(n; x,y:2*//(x LangOf(Auto3_2)-induced Equiv y); f)
auto3_2_minimization
Thm* n:, f:(n(x,y:1*//(x LangOf(Auto3_1)-induced Equiv y))).
Bij(n; x,y:1*//(x LangOf(Auto3_1)-induced Equiv y); f)
auto3_1_minimization
Thm* n:, f:(n(x,y:3*//(x LangOf(Auto
)-induced Equiv y))).
Bij(n; x,y:3*//(x LangOf(Auto)-induced Equiv y); f)
auto3_minimization
Thm* n:, f:(n(x,y:2*//(x LangOf(Auto
)-induced Equiv y))).
Bij(n; x,y:2*//(x LangOf(Auto)-induced Equiv y); f)
auto2_minimization
Thm* n:, f:(n(x,y:2*//(x LangOf(Auto
)-induced Equiv y))).
Bij(n; x,y:2*//(x LangOf(Auto)-induced Equiv y); f)
auto1_minimization
In prior sections: int 1 bool 1 choice 1 int 2 list 1 finite sets list 3 autom exponent relation autom det automata myhill nerode automata 5