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
s:(2
n). a:n. (s+(2a)) rem (2n)),0,(s:(2n). s=
0 
s=(2n)-1) >
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