DISP	auto1_df	Auto== Auto
ABS	auto1	Auto == <s,a.s, 0, s.tt>
THM	auto1_wf	Auto Automata(2;2)
THM	auto1_minimization	n: f:n x,y:(2 List)//(x Rl y). Bij(n;x,y:(2 List)//(x Rl 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!
DISP	auto2_df	Auto== Auto
ABS	auto2	Auto == <s,a.2 - s, 0, s.(s = 0)>
THM	auto2_wf	Auto Automata(2;3)
THM	auto2_minimization	n: f:n x,y:(2 List)//(x Rl y). Bij(n;x,y:(2 List)//(x Rl y);f)
DISP	auto3_df	Auto== Auto
ABS	auto3	Auto == <s,a.a, 0, s.(s = 0)>
THM	auto3_wf	Auto Automata(3;3)
THM	auto3_minimization	n: f:n x,y:(3 List)//(x Rl y). Bij(n;x,y:(3 List)//(x Rl y);f)
DISP	auto3_1_df	Auto3_1== Auto3_1
ABS	auto3_1	Auto3_1 == <s,a.a, 0, s.tt>
THM	auto3_1_wf	Auto3_1 Automata(1;1)
THM	auto3_1_minimization	n: f:n x,y:(1 List)//(x Rl y). Bij(n;x,y:(1 List)//(x Rl y);f)
DISP	auto3_2_df	Auto3_2== Auto3_2
ABS	auto3_2	Auto3_2 == <s,a.a, 0, s.tt>
THM	auto3_2_wf	Auto3_2 Automata(2;2)
THM	auto3_2_minimization	n: f:n x,y:(2 List)//(x Rl y). Bij(n;x,y:(2 List)//(x Rl y);f)
DISP	auto3_23_df	auto3_23()== auto3_23()
ABS	auto3_23	auto3_23() == <s,a.a, 0, s.tt>
THM	auto3_23_wf	auto3_23() Automata(2;3)
THM	auto3_23_minimization	n: f:n x,y:(2 List)//(x Rl y). Bij(n;x,y:(2 List)//(x Rl y);f)
DISP	auto3_3_df	auto3_3()== auto3_3()
ABS	auto3_3	auto3_3() == <s,a.a, 0, s.tt>
THM	auto3_3_wf	auto3_3() Automata(3;3)
THM	auto3_3_minimization	n: f:n x,y:(3 List)//(x Rl y). Bij(n;x,y:(3 List)//(x Rl y);f)
DISP	auto4_df	Auto4== Auto4
ABS	auto4	Auto4 == <s,a.1 - s, 0, s.(s = 0)>
THM	auto4_wf	Auto4 Automata(2;2)
THM	auto4_minimization	n: f:n x,y:(2 List)//(x Rl y). Bij(n;x,y:(2 List)//(x Rl y);f)

the other theories