LP, the Larch Prover -- Proofs of logical equivalence


The command prove t1 <=> t2 by <=> directs LP to prove the conjecture by proving two implications, t1 => t2 and t2 => t1. LP substitutes new constants for the free variables in both t1 and t2 to obtain terms t1' and t2', and it creates two subgoals: the first involves proving t2' using t1' as an additional hypothesis, the second proving t1' using t2' as an additional hypothesis. The names of the hypotheses have the form <simpleId>ImpliesHyp.<number>, where <simpleId> is the current value of the name-prefix setting.

The command resume by <=> 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 t1 <=> t2 or of the form t1 = t2 when t1 and t2 are boolean-valued terms.