// Folder
maj_inv(x, !x, y) -> y
maj_inv(x, x, y) -> x
maj_inv(x, 0, 1) -> x
// Canonicalization
maj_inv(x, y, maj_inv(x, y, z)) ->(Distribute) maj(maj(x, y, x), maj(x, y, y), z) -> maj(x, y, z)
maj_inv(x, y, maj_inv(x, not y,z)) -> (Complementary Associativity) maj_inv(x, y, maj_inv(x, x, z)) -> maj_inv(x, y, z)