automata 6 Sections AutomataTheory Doc

Def Auto4 == < (s,a. 1-s),0,(s.s=0) >

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