DISP	languages_df	L{<i:l>}(<Alph:Alph:*>)== L{<i>}(<Alph>) L(<Alph:Alph:*>)== L(<Alph>)
ABS	languages	L(Alph) == Alph List
THM	languages_wf	Alph:. L(Alph) '
DISP	lang_union_df	(<L:L:*> U <M:M:*>)== (<L> U <M>)
ABS	lang_union	(L U M) == l.L l M l
THM	lang_union_wf	Alph:. M,N:L(Alph). (M U N) L(Alph)
DISP	lang_inters_df	(<L:L:*> <M:M:*>)== (<L> <M>)
ABS	lang_inters	(L M) == l.L l M l
THM	lang_inters_wf	Alph:. M,N:L(Alph). (M N) L(Alph)
DISP	lang_compl_df	(<L:L:*>)== (<L>)
ABS	lang_compl	(L) == l.(L l)
THM	lang_compl_wf	Alph:. M:L(Alph). (M) L(Alph)
DISP	lang_prod_df	(<L:L:*><M:M:*>)== (<L><M>)
ABS	lang_prod	(LM) == l.i:{0...||l||}. L l[0..i] M l[i..||l||]
THM	lang_prod_wf	Alph:. M,N:L(Alph). (MN) L(Alph)
DISP	lang_sing_df	==
ABS	lang_sing	== l.null(l)
THM	lang_sing_wf	Alph:. L(Alph)
DISP	lang_power_df	(<L:lang:*><n:nat:*>)== (<L><n>)
ML	lang_power_ml	(Ln)==r if (n = 0) then else ((Ln - 1)L) fi
THM	lang_power_wf	Alph:. L:L(Alph). n:. (Ln) L(Alph)
THM	comb_for_lang_power_wf	(Alph,L,n,z.(Ln)) Alph: L:L(Alph) n: True L(Alph)
DISP	lang_closure_df	(<L:L:*>)== (<L>)
ABS	lang_closure	(L) == l.n:. (Ln) l
THM	lang_closure_wf	Alph:. L:L(Alph). (L) L(Alph)
DISP	lang_eq_df	<L:lang:*> = <M:lang:*> in <Alph:Alph:*>== <L> = <M> <L:L:*> = <M:M:*>== <L> = <M>
ABS	lang_eq	L = M == l:Alph List. L l M l
THM	lang_eq_wf	Alph:. L,M:L(Alph). L = M '
ML	lang_eq_ml	declare_equiv_rel `lang_eq` `equal`;;
THM	comb_for_lang_eq_wf	(Alph,L,M,z.L = M) Alph: L:L(Alph) M:L(Alph) True '
THM	lang_eq_weakening	Alph:. L,M:L(Alph). L = M L = M
THM	lang_eq_inversion	Alph:. L,M:L(Alph). L = M M = L
THM	lang_eq_transitivity	Alph:. L,M,N:L(Alph). L = M M = N L = N
THM	apply_functionality_wrt_lang_eq	Alph:. l,l':Alph List. L,L':L(Alph). L = L' l = l' (L l L' l')
THM	lang_union_functionality	Alph:. L,L',M,M':L(Alph). L = L' M = M' (L U M) = (L' U M')
THM	lang_inters_functionality	Alph:. L,L',M,M':L(Alph). L = L' M = M' (L M) = (L' M')
THM	lang_compl_functionality	Alph:. L,L':L(Alph). L = L' (L) = (L')
THM	lang_prod_functionality	Alph:. L,L',M,M':L(Alph). L = L' M = M' (LM) = (L'M')
THM	lang_power_functionality	Alph:. L,L':L(Alph). n,n':. L = L' n = n' (Ln) = (L'n')
THM	lang_closure_functionality	Alph:. L,L':L(Alph). L = L' (L) = (L')
THM	lang_union_idemp	Alph:. L:L(Alph). (L U L) = L
THM	lang_union_commut	Alph:. L,M:L(Alph). (L U M) = (M U L)
THM	lang_union_assoc	Alph:. L,M,N:L(Alph). (L U (M U N)) = ((L U M) U N)
THM	lang_union_inters	Alph:. L,M,N:L(Alph). (L U (M N)) = ((L U M) (L U N))
THM	lang_inters_idemp	Alph:. L:L(Alph). (L L) = L
THM	lang_inters_commut	Alph:. L,M:L(Alph). (L M) = (M L)
THM	lang_inters_assoc	Alph:. L,M,N:L(Alph). (L (M N)) = ((L M) N)
THM	lang_inters_union	Alph:. L,M,N:L(Alph). (L (M U N)) = ((L M) U (L N))
THM	lang_prod_sing	Alph:. L:L(Alph). (L) = L
THM	lang_sing_prod	Alph:. L:L(Alph). (L) = L
DISP	lang_empty_df	==
ABS	lang_empty	== l.False
THM	lang_empty_wf	Alph:. L(Alph)
THM	lang_zero_power	Alph:. L:L(Alph). (L0) =

the other theories