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
== < (
s,a. 2-s),0,(s.s=0) >
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