ACL2-pc::demote
(primitive)
move top-level hypotheses to the conclusion
Examples:
demote -- demote all top-level hypotheses
(demote 3 5) -- demote hypotheses 3 and 5
For example, if the top-level hypotheses are x and y and the
conclusion is z, then after execution of demote, the conclusion will
be (implies (and x y) z) and there will be no (top-level) hypotheses.
General Form:
(demote &rest hyps-indices)
Eliminate the indicated (top-level) hypotheses, but replace the conclusion
conc with (implies hyps conc) where hyps is the conjunction of
the hypotheses that were eliminated. If no arguments are supplied, then all
hypotheses are demoted, i.e. demote is the same as (demote 1 2
... n) where n is the number of top-level hypotheses.
Remark: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke top. Also, demote fails if
there are no top-level hypotheses or if indices are supplied that are out of
range.
