useful selection identities

bdd_select.txt

(c f t) <> select(c,t,f) <> c?t:f <> !c&f | c&t

0 = (x 0 0) = (0 0 x) = (x x 0) = (x 0 !x)
1 = (x 1 1) = (1 x 1) = (x 1 x) = (x !x 1)

x = (x 0 1) = (1 y x) = (0 x y) = (x 0 x) = (x x 1) = (y x x)
!x = (x 1 0) = (x !x 0) = (x 1 !x)

(!a b c) = (a c b)
!(a b c) = (a !b !c)

a & b = (a 0 b) = (b 0 a)
!a & b = (a b 0) = (b 0 !a)
!a & !b = (a !b 0) = (b !a 0)

a | b = (a b 1) = (b a 1)
!a | b = (a 1 b) = (b !a 1)
!a | !b = (a 1 !b) = (b 1 !a)

a ^ b = (a b !b)

(x f(x) g(x)) = (x f(0) g(1))

((a b c) d e) = (a (b d e) (c d e))

a & b | c  = (a c (b c 1)) = (c (a 0 b) 1)
a & (b | c) = (a 0 (b c 1)) = (b (a 0 c) a)

!a&b | a&c
        = ((a b 0) (a 0 c) 1)
        = (a (b (a 0 c) 1) (0 (a 0 c) 1))   | isolate a
        = (a (b (0 0 c) 1) (1 0 c))         | substitute a
        = (a (b 0 1) c)
        = (a b c)