| -- 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; | |