Nand theorems

The total number of expressions with n Nands and s variables is: Binomial[2n, n]s^{n + 1}/(n + 1) (see page 897). With s = 2 and n from 0 to 7 the number of these True for all values of variables is {0, 0, 4, 0, 80, 108, 2592, 7296}, with the first few distinct ones being (see page 781)

{(p ⊼ p) ⊼ p, (((p ⊼ p) ⊼ p) ⊼ p) ⊼ p, (((p ⊼ p) ⊼ p) ⊼ q) ⊼ q}

The number of unequal expressions obtained is {2, 3, 3, 7, 10, 15, 12, 16} (compare page 1096), with the first few distinct ones being

{p, p ⊼ p, p ⊼ q, (p ⊼ p) ⊼ p, (p ⊼ q) ⊼ p, (p ⊼ p) ⊼ q}

Most of the axioms from page 808 are too long to appear early in the list of theorems. But those of system (d) appear at positions {3, 15, 568} and those of (e) at {855, 4}.

(See also page 1096.)