acl2This user proves theorems using ACL2.