Selected Objects

def	lang_rel	L-induced Equiv(x,y) == z:A*. L(z @ x) L(z @ y)
THM	lang_rel_refl	L:LangOver(A). Refl(A*;x,y.x L-induced Equiv y)
THM	lang_rel_symm	L:LangOver(A). Sym x,y:A*. x L-induced Equiv y
THM	lang_rel_tran	L:LangOver(A). Trans x,y:A*. x L-induced Equiv y
THM	lang_rel_equi	L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y
def	mn_quo_append	z@x == z @ x
THM	mn_quo_append_assoc	R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (z1,z2:Alph*, y:x,y:Alph*//(x R y). z1 @ z2@y = z1@z2@y)
def	lquo_rel	Rg(x,y) == z:A*. g(z@x) g(z@y)
THM	lquo_rel_refl	R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). Refl(x,y:A*//(x R y);u,v.u Rg v))
THM	lquo_rel_symm	R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). Sym u,v:x,y:A*//(x R y). u Rg v)
THM	lquo_rel_tran	R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). Trans u,v:x,y:A*//(x R y). u Rg v)
THM	lquo_rel_equi	R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). EquivRel u,v:x,y:A*//(x R y). u Rg v)
THM	Rl_iff_Rg	R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))), L:LangOver(A). (l:A*. L(l) g(l)) (x,y:A*. (x L-induced Equiv y) (x Rg y)))
THM	mn_12	L:LangOver(Alph). Fin(Alph) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto)) (R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) c (g:((x,y:Alph*//R(x,y))). Fin(x,y:Alph*//R(x,y)) & (l:Alph*. L(l) g(l)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))))
THM	mn_23_refinment	L:LangOver(Alph), R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (g:((x,y:Alph*//(x R y))). l:Alph*. L(l) g(l)) & (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (x,y:Alph*. (x R y) (x L-induced Equiv y))
def	beq	p = q == if p q else q fi
THM	beq_id	p:. p = p = true
THM	beq_sym	p,q:. p = q = q = p
THM	beq_eq	p,q:. p = q = true p = q
THM	beq_neq	p,q:. p = q = false p = q
THM	assert_iff_eq	a,b:. (a b) a = b
THM	mn_23_lem_0	P:(Prop), n:. (k:{n...}. P(k) (i:k. P(i))) & (m:. P(m)) (m:n. P(m))
THM	fin_listify	Fin(T) (TL:T*. t:T. mem_f(T;t;TL))
THM	back_listify	S:ActionSet(Alph), s:S.car. Fin(Alph) Fin(S.car) (BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s))
THM	bool_listify	f:(T). Fin(T) (fL:T*. t:T. f(t) mem_f(T;t;fL))
THM	total_back_listify	S:ActionSet(Alph), sL:S.car*. Fin(Alph) Fin(S.car) (TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL)))
THM	mn_23_lem	R:(Alph*Alph*Prop). Fin(Alph) (EquivRel x,y:Alph*. x R y) Fin(x,y:Alph*//(x R y)) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
THM	mn_23_lem_1	R:(Alph*Alph*Prop). Fin(Alph) (EquivRel x,y:Alph*. x R y) Fin(x,y:Alph*//(x R y)) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
THM	nxn_plus_1_ge_0	n:. nn+1
THM	mn_23_Rl_equal_Rg	L:LangOver(Alph), R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:Alph*//(x R y))). (l:Alph*. L(l) g(l)) x,y:Alph*//(x L-induced Equiv y) = x,y:Alph*//(x Rg y))
THM	mn_23	n:{1...}, A:Type, L:LangOver(A), R:(A*A*Prop). Fin(A) (EquivRel x,y:A*. x R y) (n ~ (x,y:A*//(x R y))) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). l:A*. L(l) g(l)) (m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l)))
THM	mn_31	L:LangOver(Alph). Fin(Alph) Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l))) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))