		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::reduce

(atomic macro) call the ACL2 theorem prover's simplifier

Examples:
reduce -- attempt to prove the current goal without using induction
(reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
       -- attempt to prove the current goal without using
          induction, with the indicated hints

General Form:
(reduce &rest hints)

Attempt to prove the current goal without using induction, using the indicated hints (if any). A subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof.

Notice that unlike prove, the arguments to reduce are spread out, and are all hints.

Reduce is similar to bash in that neither of these allows induction. But bash only allows simplification, while reduce allows processes eliminate-destructors, fertilize, generalize, and eliminate-irrelevance.

Remark: Induction will be used to the extent that it is ordered explicitly in the hints.