		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::forwardchain

(atomic macro) forward chain from an implication in the hyps

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 the given index. That hypothesis — call it H — must be of the form (IMPLIES hyp concl). The effect of this command is to replace H by concl, which becomes the final hypothesis.

The prover must be able to prove concl from the hypotheses other than H (more precisely, to prove concl after removing the hypothesis at the given index), 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.