DISP	lang_rel_df	Rl== Rl
ABS	lang_rel	Rl == x,y.z:A List. L (z @ x) L (z @ y)
THM	lang_rel_wf	A:. L:L(A). Rl A List A List
THM	lang_rel_refl	A:. L:L(A). Refl(A List;x,y.x Rl y)
THM	lang_rel_symm	A:. L:L(A). Sym(A List;x,y.x Rl y)
THM	lang_rel_tran	A:. L:L(A). Trans(A List;x,y.x Rl y)
THM	lang_rel_equi	A:. L:L(A). EquivRel(A List;x,y.x Rl y)
DISP	mn_quo_append_df	<z:z:*>@<x:x:*>== <z>@<x>
ABS	mn_quo_append	z@x == z @ x
THM	mn_quo_append_wf	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (z:A List. y:x,y:(A List)//(x R y). z@y x,y:(A List)//(x R y))
THM	mn_quo_append_assoc	Alph:. R:Alph List Alph List . EquivRel(Alph List;x,y.x R y) (x,y,z:Alph List. x R y (z @ x) R (z @ y)) (z1,z2:Alph List. y:x,y:(Alph List)//(x R y). z1 @ z2@y = z1@z2@y)
DISP	lquo_rel_df	Rg== Rg
ABS	lquo_rel	Rg == x,y.z:A List. (g z@x) (g z@y)
THM	lquo_rel_wf	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) Rg x,y:(A List)//(x R y) x,y:(A List)//(x R y) )
THM	lquo_rel_refl	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) Refl(x,y:(A List)//(x R y);u,v.u Rg v))
THM	lquo_rel_symm	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) Sym(x,y:(A List)//(x R y);u,v.u Rg v))
THM	lquo_rel_tran	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) Trans(x,y:(A List)//(x R y);u,v.u Rg v))
THM	lquo_rel_equi	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) EquivRel(x,y:(A List)//(x R y);u,v.u Rg v))
THM	Rl_iff_Rg	A:. R:A List A List . EquivRel(A List;x,y.x R y) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) . L:L(A). (l:A List. L l (g l)) (x,y:A List. x Rl y x Rg y))
THM	mn_12	Alph:. L:L(Alph). Fin(Alph) (St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto)) (R:Alph List Alph List EquivRel(Alph List;x,y.x R y) c (g:x,y:(Alph List)//(R x y) Fin(x,y:(Alph List)//(R x y)) (l:Alph List. L l (g l)) (x,y,z:Alph List. R x y R (z @ x) (z @ y))))
THM	mn_23_refinment	Alph:. L:L(Alph). R:Alph List Alph List . EquivRel(Alph List;x,y.x R y) (g:x,y:(Alph List)//(x R y) . l:Alph List. L l (g l)) (x,y,z:Alph List. x R y (z @ x) R (z @ y)) (x,y:Alph List. x R y x Rl y)
DISP	beq_df	<p:bool> = <q:bool:E>== <p> = <q>
ABS	beq	p = q == if p then q else q fi
THM	beq_wf	p,q:. p = q
THM	beq_id	p:. p = p = tt
THM	beq_sym	p,q:. p = q = q = p
THM	beq_eq	p,q:. p = q = tt p = q
THM	beq_neq	p,q:. p = q = ff p = q
THM	assert_iff_eq	a,b:. (a b) a = b
THM	mn_23_lem_0	P: . n:. (k:{n...}. P k (i:k. P i)) (m:. P m) (m:n. P m)
THM	fin_listify	T:. Fin(T) (TL:T List. t:T. mem_f(T;t;TL))
THM	back_listify	Alph:. S:ActionSet(Alph). s:S.car. Fin(Alph) Fin(S.car) (BL:S.car List t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act a t = s))
THM	bool_listify	T:. f:T . Fin(T) (fL:T List. t:T. (f t) mem_f(T;t;fL))
THM	total_back_listify	Alph:. S:ActionSet(Alph). sL:S.car List. Fin(Alph) Fin(S.car) (TBL:S.car List s:S.car mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL)))
THM	mn_23_lem	Alph:. R:Alph List Alph List . Fin(Alph) EquivRel(Alph List;x,y.x R y) Fin(x,y:(Alph List)//(x R y)) (x,y,z:Alph List. x R y (z @ x) R (z @ y)) (g:x,y:(Alph List)//(x R y) . x,y:x,y:(Alph List)//(x R y). Dec(x Rg y))
THM	mn_23_lem_1	Alph:. R:Alph List Alph List . Fin(Alph) EquivRel(Alph List;x,y.x R y) Fin(x,y:(Alph List)//(x R y)) (x,y,z:Alph List. x R y (z @ x) R (z @ y)) (g:x,y:(Alph List)//(x R y) . x,y:x,y:(Alph List)//(x R y). Dec(x Rg y))
THM	nxn_plus_1_ge_0	n:. n * n + 1
THM	mn_23_Rl_equal_Rg	Alph:. L:L(Alph). R:Alph List Alph List . EquivRel(Alph List;x,y.x R y) (x,y,z:Alph List. x R y (z @ x) R (z @ y)) (g:x,y:(Alph List)//(x R y) (l:Alph List. L l (g l)) x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rg y))
THM	mn_23	n:{1...}. A:. L:L(A). R:A List A List . Fin(A) EquivRel(A List;x,y.x R y) 1-1-Corresp(n;x,y:(A List)//(x R y)) (x,y,z:A List. x R y (z @ x) R (z @ y)) (g:x,y:(A List)//(x R y) . l:A List. L l (g l)) (m:. 1-1-Corresp(m;x,y:(A List)//(x Rl y))) (l:A List. Dec(L l))
THM	mn_31	Alph:. L:L(Alph). Fin(Alph) Fin(x,y:(Alph List)//(Rl x y)) (l:Alph List. Dec(L l)) (St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))

the other theories