-- gates.nf — All standard gates from NAND alone
-- NOT, AND, OR, XOR — each built purely from NAND

module gates;

-- NOT x = x NAND x
def not(x) = (x | x);

-- AND x y = NOT (x NAND y)
def and(x y) = not((x | y));

-- OR x y = (NOT x) NAND (NOT y)
def or(x y) = (not(x) | not(y));

-- XOR x y = (x NAND (x NAND y)) NAND (y NAND (x NAND y))
def xor(x y) = ((x | (x | y)) | (y | (x | y)));

-- Proofs: derived gates are correct
prove not_true:  not(true) = false;
prove not_false: not(false) = true;

prove and_tt: and(true true) = true;
prove and_tf: and(true false) = false;
prove and_ft: and(false true) = false;
prove and_ff: and(false false) = false;

prove or_tt: or(true true) = true;
prove or_tf: or(true false) = true;
prove or_ft: or(false true) = true;
prove or_ff: or(false false) = false;

prove xor_tt: xor(true true) = false;
prove xor_tf: xor(true false) = true;
prove xor_ft: xor(false true) = true;
prove xor_ff: xor(false false) = false;