|
|
|---|
|
|
|
|---|
(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 given index, which
should be of the form
The prover must be able to prove the indicated hypothesis from the other
hypotheses, or else the command will fail. The
Output is suppressed if