# LP, the Larch Prover -- Proofs of conditionals

Proofs of formulas involving the conditional operator `if` can be carried
out using a simplified proof by cases. The commands
`prove if t1 then t2 else t3 by if-method
prove (if t1 then t2 else t3) = t4 by if-method
`

direct LP to prove the conjectures by division into two cases, `t1` and
`~t1`. LP substitutes new constants for the free
variables of `t1` in all terms `ti` to obtain terms `ti'`. In the
first case, it assumes `t1'` as an additional hypothesis and attempts to
prove `t2'` (or `t2' = t4'`) as a subgoal. In the second case, it
assumes `t1' = false` as an additional hypothesis and attempts to prove
`t3'` (or `t3' = t4'`). The names of the hypotheses have the form
<simpleId>`IfHyp.`<number>, where <simpleId> is the current value of
the name-prefix setting.
The command `resume by if-method` directs LP to resume the proof of the
current conjecture using this method. It is applicable only when the current
conjecture has been reduced to a formula of the form `if t1 then t2 else t3`
or of the form `(if t1 then t2 else t3) = t4`, where `t4` does not begin
with `if`.