Just to look at, here are the actual machine proofs from running our verifier theory through the Boyer-Moore prover.[1] AI, the early years, at work. Here's one proof, for commutativity of TIMES for the natural numbers.

    (PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE) (EQUAL (TIMES X Y) (TIMES Y X)))
    
         Give the conjecture the name *1.
    
         We will appeal to induction.  Two inductions are suggested by terms in
    the conjecture, both of which are flawed.  We limit our consideration to the
    two suggested by the largest number of nonprimitive recursive functions in the
    conjecture.  Since both of these are equally likely, we will choose
    arbitrarily.  We will induct according to the following scheme:
          (AND (IMPLIES (ZEROP X) (p X Y))
               (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                        (p X Y))).
    Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
    us that the measure (COUNT X) decreases according to the well-founded relation
    LESSP in each induction step of the scheme.  The above induction scheme
    produces the following two new conjectures:
    
    Case 2. (IMPLIES (ZEROP X)
                     (EQUAL (TIMES X Y) (TIMES Y X))).
    
      This simplifies, applying TIMES-ZERO and TIMES-NON-NUMBERP, and opening up
      the functions ZEROP, EQUAL, and TIMES, to:
    
            T.
    
    Case 1. (IMPLIES (AND (NOT (ZEROP X))
                          (EQUAL (TIMES (SUB1 X) Y)
                                 (TIMES Y (SUB1 X))))
                     (EQUAL (TIMES X Y) (TIMES Y X))),
    
      which simplifies, unfolding the functions ZEROP and TIMES, to:
    
            (IMPLIES (AND (NOT (EQUAL X 0))
                          (NUMBERP X)
                          (EQUAL (TIMES (SUB1 X) Y)
                                 (TIMES Y (SUB1 X))))
                     (EQUAL (PLUS Y (TIMES Y (SUB1 X)))
                            (TIMES Y X))).
    
      Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
      (SUB1 X).  We employ the type restriction lemma noted when SUB1 was
      introduced to constrain the new variable.  We must thus prove:
    
            (IMPLIES (AND (NUMBERP Z)
                          (NOT (EQUAL (ADD1 Z) 0))
                          (EQUAL (TIMES Z Y) (TIMES Y Z)))
                     (EQUAL (PLUS Y (TIMES Y Z))
                            (TIMES Y (ADD1 Z)))).
    
      However this further simplifies, applying the lemma TIMES-ADD1, to:
    
            T.
    
    
    That finishes the proof of *1. Q.E.D.

Boyer and Moore were trying really hard to make the results understandable to traditional mathematicians.

[1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...