-- mux.nf — 2-to-1 multiplexer from NAND
-- mux(sel, a, b) = if sel then b else a

module mux;

def not(x) = (x | x);
def and(x y) = not((x | y));
def or(x y) = (not(x) | not(y));

-- MUX: output = (NOT sel AND a) OR (sel AND b)
def mux(sel a b) = or(and(not(sel) a) and(sel b));

-- sel=0 selects input a
prove mux_0_a0_b0: mux(false false false) = false;
prove mux_0_a0_b1: mux(false false true) = false;
prove mux_0_a1_b0: mux(false true false) = true;
prove mux_0_a1_b1: mux(false true true) = true;

-- sel=1 selects input b
prove mux_1_a0_b0: mux(true false false) = false;
prove mux_1_a0_b1: mux(true false true) = true;
prove mux_1_a1_b0: mux(true true false) = false;
prove mux_1_a1_b1: mux(true true true) = true;