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:.
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:, 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: fun 1 finite sets exponent relation autom