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.
