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.prove if t1 then t2 else t3 by if-method prove (if t1 then t2 else t3) = t4 by if-method
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.