LP uses active rewrite rules to normalize conjectures. If a conjecture normalizes to

from the axioms{e} \subseteq insert(e, s)

by using them to reduce it to{e} = insert(e, {}) e \in insert(e1, x) <=> e = e1 \/ e \in s {} \subseteq s insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y

Passive rewrite rules can be applied explicitly to a conjecture by the normalize and rewrite commands. These commands can be used to control when definitions are expanded, or when nonsimplifying rewrite rules (such as distributivity) are applied.