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.