Selected Objects

def	languages	LangOver(Alph) == Alph*Prop
def	lang_union	(L U M)(l) == L(l) M(l)
def	lang_inters	(L M)(l) == L(l) & M(l)
def	lang_compl	(L)(l) == L(l)
def	lang_prod	(LM)(l) == i:{0...||l||}. L(l[0..i]) & M(l[i..||l||])
def	lang_sing	(l) == null(l)
def	lang_power	(rec) (Ln) == if n=0 else ((Ln-1)L) fi
def	lang_closure	(L)(l) == n:. (Ln)(l)
def	lang_eq	L = M == l:Alph*. L(l) M(l)
THM	lang_eq_weakening	L,M:LangOver(Alph). L = M L = M
THM	lang_eq_inversion	L,M:LangOver(Alph). L = M M = L
THM	lang_eq_transitivity	L,M,N:LangOver(Alph). L = M M = N L = N
THM	apply_functionality_wrt_lang_eq	l,l':Alph*, L,L':LangOver(Alph). L = L' l = l' (L(l) L'(l'))
THM	lang_union_functionality	L,L',M,M':LangOver(Alph). L = L' M = M' (L U M) = (L' U M')
THM	lang_inters_functionality	L,L',M,M':LangOver(Alph). L = L' M = M' (L M) = (L' M')
THM	lang_compl_functionality	L,L':LangOver(Alph). L = L' (L) = (L')
THM	lang_prod_functionality	L,L',M,M':LangOver(Alph). L = L' M = M' (LM) = (L'M')
THM	lang_power_functionality	L,L':LangOver(Alph), n,n':. L = L' n = n' (Ln) = (L'n')
THM	lang_closure_functionality	L,L':LangOver(Alph). L = L' (L) = (L')
THM	lang_union_idemp	L:LangOver(Alph). (L U L) = L
THM	lang_union_commut	L,M:LangOver(Alph). (L U M) = (M U L)
THM	lang_union_assoc	L,M,N:LangOver(Alph). (L U (M U N)) = ((L U M) U N)
THM	lang_union_inters	L,M,N:LangOver(Alph). (L U (M N)) = ((L U M) (L U N))
THM	lang_inters_idemp	L:LangOver(Alph). (L L) = L
THM	lang_inters_commut	L,M:LangOver(Alph). (L M) = (M L)
THM	lang_inters_assoc	L,M,N:LangOver(Alph). (L (M N)) = ((L M) N)
THM	lang_inters_union	L,M,N:LangOver(Alph). (L (M U N)) = ((L M) U (L N))
THM	lang_prod_sing	L:LangOver(Alph). (L) = L
THM	lang_sing_prod	L:LangOver(Alph). (L) = L
def	lang_empty	(l) == False
THM	lang_zero_power	L:LangOver(Alph). (L0) =