ACL2 Is Fascinating

:::lisp
ACL2 !> (thm (=(+ a b) (+ b a)))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION =)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  10

Proof succeeded.