<assert-command> ::= assert <assertion>;+ [;] <assertion> ::= [:<simpleId>:] <fact> <fact> ::= <formula> | <deduction-rule> | <induction-rule> | <operator-theory> | <partitioned-by>
assert e1 \in insert(e2, s) <=> e1 = e2 \/ e1 \in s; when \A e (e \in s1 <=> e \in s2) yield s1 = s2; Set generated by {}, insert; ac \U; Set partitioned by \in ..
LP takes certain default actions when it adds assertions to its logical system.