Selected Objects

def	auto1	Auto == < (s,a. s),0,(s.true) >
THM	auto1_minimization	n:, f:(n(x,y:2*//(x LangOf(Auto)-induced Equiv y))). Bij(n; x,y:2*//(x LangOf(Auto)-induced Equiv y); f)
COM	auto1_howto	If you want to get number of state in minimal automata that accepts the same language as 'Auto' just type term_to_string (evaluate_term 'ext{auto1_minimization}') into your ML top loop. But keep in mind that in order to get 'ext{auto1_minimization}' you will need to open a term slot with Ctrl+o and type in "auto1_minimization". In several minutes you will get lots of line as output. Just look for a first number!
def	auto2	Auto == < (s,a. 2-s),0,(s.s=0) >
THM	auto2_minimization	n:, f:(n(x,y:2*//(x LangOf(Auto)-induced Equiv y))). Bij(n; x,y:2*//(x LangOf(Auto)-induced Equiv y); f)
def	auto3	Auto == < (s,a. a),0,(s.s=0) >
THM	auto3_minimization	n:, f:(n(x,y:3*//(x LangOf(Auto)-induced Equiv y))). Bij(n; x,y:3*//(x LangOf(Auto)-induced Equiv y); f)
def	auto3_1	Auto3_1 == < (s,a. a),0,(s.true) >
THM	auto3_1_minimization	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)
def	auto3_2	Auto3_2 == < (s,a. a),0,(s.true) >
THM	auto3_2_minimization	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)
def	auto3_23	auto3_23() == < (s,a. a),0,(s.true) >
THM	auto3_23_minimization	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)
def	auto3_3	auto3_3() == < (s,a. a),0,(s.true) >
THM	auto3_3_minimization	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)
def	auto4	Auto4 == < (s,a. 1-s),0,(s.s=0) >
THM	auto4_minimization	n:, f:(n(x,y:2*//(x LangOf(Auto4)-induced Equiv y))). Bij(n; x,y:2*//(x LangOf(Auto4)-induced Equiv y); f)
def	auto_oddeven	OddEven#n == < (s:(2n). a:n. (s+(2a)) rem (2n)),0,(s:(2n). s=0 s=(2n)-1) >
THM	oddeven_minimization	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)