# LP, the Larch Prover -- The apply command

The *apply command* provides manual control over the application of
(possibly passive) deduction rules to (possibly immune) formulas and rewrite
rules. It also provides a means of backward inference for finishing the proof
of a conjecture.
`<apply-command> ::= ``apply` <names> `to` <target>
<target> ::= <names> | `conjecture`

## Examples

`apply passive / deduction-rules to *
apply setExtensionality to conjecture
`

## Usage

The first version of the `apply` command applies the named
deduction rules,
whether or not they are active, to the formulas
and rewrite rules named as the <target>, whether or not they are
immune.
The second version attempts to prove the current conjecture by explicit
deduction using the named deduction rules. The attempt succeeds if the current
conjecture matches a conclusion of a named deduction rule and the hypotheses of
that deduction rule, under the matching substitution, reduce to `true`.
For example, if LP's logical system contains the axioms

`setAxioms.1: e \in (x \U y) -> e \in x \/ e \in y
setExtensionality.1: when \A e (e \in s1 <=> e \in s2) yield s1 = s2
`

then the command `apply setExtensionality to conjecture` finishes the proof
of the conjecture `x \U x = x`.