-- half_adder.nf — Binary addition from NAND
-- sum = XOR(a, b), carry = AND(a, b)

module half_adder;

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

def sum(a b) = xor(a b);
def carry(a b) = and(a b);

-- 0 + 0 = 00
prove sum_00: sum(false false) = false;
prove carry_00: carry(false false) = false;

-- 0 + 1 = 01
prove sum_01: sum(false true) = true;
prove carry_01: carry(false true) = false;

-- 1 + 0 = 01
prove sum_10: sum(true false) = true;
prove carry_10: carry(true false) = false;

-- 1 + 1 = 10
prove sum_11: sum(true true) = false;
prove carry_11: carry(true true) = true;