\doc{The assert command}
\ref{assertions}
\ref{assert-command}
\ref{facts}
\ref{axioms}

The \def{assert command} adds axioms to LP's logical system.

\head{2}{\dlink{../symbols/syntax}{Syntax}}
\begin{verbatim}
\sd{assert-command} ::= \f{assert} \s{assertion};+ [;]
\sd{assertion}      ::= [\f{:}\s{simpleId}\f{:}] \s{fact}
\sd{fact}           ::= \slink{../logic/formula}{formula} | \slink{../logic/deduction-rule}{deduction-rule} | \slink{../logic/induction-rule}{induction-rule} 
                        | \slink{../logic/operator-theory}{operator-theory} | \slink{../logic/partitioned-by}{partitioned-by}
\end{verbatim}

\head{2}{Examples}
\begin{verbatim}
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
  ..
\end{verbatim}

\head{2}{Usage}

LP adds the asserted facts to its logical system.  It assigns a
\dlink{../misc/name}{name} to each of these facts using the current 
\setlink{name-prefix} setting, unless an assertion begins with 
\f{:}\s{simpleId}\f{:}, in which case LP uses that identifier as the
name-prefix for that assertion.
\p
LP takes certain default actions when it adds assertions to its logical system.
\begin{itemize}
\item
It translates \s{partitioned-by}s into deduction rules.
\item
It \olink{normalization}{normalizes} asserted formulas and deduction rules
(unless the \setlink{immunity} setting dictates otherwise).
\item
It attempts to \dlink{order}{orient} asserted formulas into
terminating \llink{rewrite-rule}{rewrite rules} (unless the 
\setlink{automatic-ordering} setting dictates otherwise).
\item
It uses new rewrite rules to normalize the other formulas and deduction rules
(unless the \setlink{activity} setting dictates otherwise).
\item
It uses new deduction rules to deduce consequences from formulas and rewrite
rules (again, unless the \setlink{activity} setting dictates otherwise).
\item
It registers operators asserted to be \f{ac} or \f{commutative} as having
multiset \dlink{../ordering/status}{status}.  If any of these operators had a
non-ac (or noncommutative) 
\dlink{../ordering/polynomial}{polynomial interpretation}, LP prints a warning 
and gives the operator a default ac (or commutative) polynomial interpretation.
\item
It turns all rewrite rules containing an operator asserted to be \f{ac} or
\f{commutative} back into formulas, and it \olink{flatten}{reflattens} all 
facts containing these operators.  This process can change these facts or even
reduce them to \fq{true}, as is the case for the commutativity equation.
\end{itemize}