LP several additional hardwired rewrite rules to simplify terms containing conditional operators. It always uses the following two rules:if true then x else y -> x if false then x else y -> y
Unless the hardwired-usage setting dictates otherwise, it also uses the following rewrite rules:if x then y else y -> y if ~x then y else z -> if x then z else y
Likewise, unless the hardwired-usage setting dictates otherwise, LP uses the if-simplification metaruleif 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
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.if t1 then t2[t1] else t3[t1] -> if t1 then t2[true] else t3[false]