Thm* L:LangOver(Alph). (L0) = lang_zero_power

Thm* L:LangOver(Alph). (L) = L lang_sing_prod

Thm* L:LangOver(Alph). (L) = L lang_prod_sing

Thm* L,M,N:LangOver(Alph). (L (M U N)) = ((L M) U (L N)) lang_inters_union

Thm* L,M,N:LangOver(Alph). (L (M N)) = ((L M) N) lang_inters_assoc

Thm* L,M:LangOver(Alph). (L M) = (M L) lang_inters_commut

Thm* L:LangOver(Alph). (L L) = L lang_inters_idemp

Thm* L,M,N:LangOver(Alph). (L U (M N)) = ((L U M) (L U N)) lang_union_inters

Thm* L,M,N:LangOver(Alph). (L U (M U N)) = ((L U M) U N) lang_union_assoc

Thm* L,M:LangOver(Alph). (L U M) = (M U L) lang_union_commut

Thm* L:LangOver(Alph). (L U L) = L lang_union_idemp

Thm* L,L':LangOver(Alph). L = L' (L) = (L') lang_closure_functionality

Thm* L,L':LangOver(Alph), n,n':. L = L' n = n' (Ln) = (L'n') lang_power_functionality

Thm* L,L',M,M':LangOver(Alph). L = L' M = M' (LM) = (L'M') lang_prod_functionality

Thm* L,L':LangOver(Alph). L = L' (L) = (L') lang_compl_functionality

Thm* L,L',M,M':LangOver(Alph). L = L' M = M' (L M) = (L' M') lang_inters_functionality

Thm* L,L',M,M':LangOver(Alph). L = L' M = M' (L U M) = (L' U M') lang_union_functionality

Thm* l,l':Alph*, L,L':LangOver(Alph). L = L' l = l' (L(l) L'(l')) apply_functionality_wrt_lang_eq

Thm* L,M,N:LangOver(Alph). L = M M = N L = N lang_eq_transitivity

Thm* L,M:LangOver(Alph). L = M M = L lang_eq_inversion

Thm* L,M:LangOver(Alph). L = M L = M lang_eq_weakening