Steps in an automated proof of the correctness of Wolfram’s Axiom
The goal is to prove as theorems the three standard Sheffer axioms of Boolean algebra from Wolfram's single axiom.
Each step states what is being proved, then gives a list of the steps required for a proof.
The result is a proof that Wolfram's Axiom is a complete axiom for Boolean algebra. It is the simplest possible one.
The proof was first given in very small type on pages 810 and 811 of "A New Kind of Science".
Each individual step in the proof is performed by inserting the specified axiom or lemma, essentially using pattern matching, but with substitutions and rearrangements for variables being made.