### ACL2-PC::REDUCE

(atomic macro)
` `

call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS

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 by 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.

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