LP, the Larch Prover -- Conditional operators

LP automatically declares a conditional operator if__then__else__ with signature Bool,S,S->S for each sort S. The meaning of this operator is given by the following two hardwired rewrite rules. 
if true then x else y  -> x
if false then x else y -> y
LP several additional hardwired rewrite rules to simplify terms containing conditional operators. It always uses the following two rules: 
if x then y else y -> y
if ~x then y else z -> if x then z else y
Unless the hardwired-usage setting dictates otherwise, it also uses the following rewrite rules: 
if x then true else y  -> x \/ y
if x then false else y -> ~x /\ y
if x then y else true  -> x => y
if x then y else false -> x /\ y
Likewise, unless the hardwired-usage setting dictates otherwise, LP uses the if-simplification metarule 
if t1 then t2[t1] else t3[t1] -> if t1 then t2[true] else t3[false]
to reduce terms when t1 occurs as a subterm of t2 or t3; here t2[true] is the result of substituting true for every occurrence of t1 as a subterm of t2, and t3[false] is defined similarly.

See also