a^ = a
^a = a
a0 = 0
0a = 0
a+0 = a
a+a = a
a+b | sub b a = a
ab+ac = a(b+c)
ac+bc = (a+b)c
(ab)*a = a(ba)*
(a+^)a = a(a+^)
(ab+c)* | ewp a, ewp b = (a+b+c)*
a+bb* | ewp a = a+b*
a+^ | ewp a = a
(a*+b)* = (a+b)*
(aa*)* = a*
a*(ba*)* = (b+a)*
(a+c)b* | sub a b*, ewp y = yb*
b*(a+c) | sub a b*, ewp y = b*y
a** = a*
