ACL2-PC::FORWARDCHAIN

(atomic macro) forward chain from an implication in the hyps
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(forwardchain 2) ; Second hypothesis should be of the form
                 ; (IMPLIES hyp concl), and the result is to replace
                 ; that hypothesis with concl.


General Forms:
(forwardchain hypothesis-number)
(forwardchain hypothesis-number hints)
(forwardchain hypothesis-number hints quiet-flg)

This command replaces the hypothesis corresponding to given index, which should be of the form (IMPLIES hyp concl), with its consequent concl. In fact, the given hypothesis is dropped, and the replacement hypothesis will appear as the final hypothesis after this command is executed.

The prover must be able to prove the indicated hypothesis from the other hypotheses, or else the command will fail. The :hints argument is used in this prover call, and should have the usual syntax of hints to the prover.

Output is suppressed if quiet-flg is supplied and not nil.