-- nand.nf — The primitive gate
-- NAND is the only primitive. Everything else is derived.

module nand;

-- NAND truth table: 0|0=1, 0|1=1, 1|0=1, 1|1=0
prove nand_not_both_true: (true | true) = false;
prove nand_false_left:    (false | true) = true;
prove nand_false_right:   (true | false) = true;
prove nand_both_false:    (false | false) = true;