### 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`

.