diff --git a/spec/alethe_rules.tex b/spec/alethe_rules.tex
deleted file mode 100644
index c9c1b4d31ce0b323202918c8f29d9f941d4cc9d6..0000000000000000000000000000000000000000
--- a/spec/alethe_rules.tex
+++ /dev/null
@@ -1,1534 +0,0 @@
-This section provides a list of all proof rules supported by
-Alethe. To make this long list more accessible, the section
-first lists multiple classes of proof rules. The classes are not
-mutually exclusive: for example, the \proofRule{la_generic} rule is
-both a linear arithmetic rule and introduces a tautology.
-The number in brackets is the position of the rule in the overall list
-of proof rules.
-Table~\ref{rule-tab:special} lists rules that serve a special purpose.
-Table~\ref{rule-tab:tautologies} lists all rules that introduce
-tautologies. That is, regular rules that do not use premises.
-
-The subsequent section, starting at ref{sec:alethe:rules-list}, defines
-all rules and provides example proofs for complicated rules.
-The index of proof rules at ref{sec:alethe:rules-index} can be used
-to quickly find the definition of rules.
-
-\subsection{Classifications of the Rules}
-\label{sec:alethe:rules-overview}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Special rules.}
-\label{rule-tab:special}\\
- Rule & Description \\
- \hline
- \ruleref{assume} & Repetition of an input assumption. \\
- \ruleref{hole} & Placeholder for rules not defined here. \\
- \ruleref{subproof} & Concludes a subproof and discharges local assumptions. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Resolution and related rules.}
-\label{rule-tab:resolution}\\
- Rule & Description \\
- \hline
- \ruleref{resolution} & Chain resolution of two or more clauses. \\
- \ruleref{th_resolution} & As \proofRule{resolution}, but used by theory solvers. \\
- \ruleref{tautology} & Simplification of tautological clauses to $\top$. \\
- \ruleref{contraction} & Removal of duplicated literals. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Rules introducing tautologies.}
-\label{rule-tab:tautologies}\\
- Rule & Description \\
- \hline
-\ruleref{true} & $\top$ \\
-\ruleref{false} & $\neg\bot$ \\
-\ruleref{not_not} & $\neg(\neg\neg\varphi), \varphi$ \\
-\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
-\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
-\ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
-\ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
-\ruleref{la_tautology} & A trivial linear tautology. \\
-\ruleref{forall_inst} & Quantifier instantiation. \\
-\ruleref{refl} & Reflexivity after applying the context. \\
-\ruleref{eq_reflexive} & $t ≈ t$ without context. \\
-\ruleref{eq_transitive} & $\neg (t_1 ≈ t_2) , \dots , \neg (t_{n-1} ≈ t_n) , t_1 ≈ t_n$ \\
-\ruleref{eq_congruent} & $\neg (t_1 ≈ u_1) , \dots , \neg (t_n ≈ u_n) , f(t_1, \dots, t_n) ≈ f(u_1, \dots, u_n)$ \\
-\ruleref{eq_congruent_pred} & $\neg (t_1 ≈ u_1) , \dots , \neg (t_n ≈ u_n) , P(t_1, \dots, t_n) ≈ P(u_1, \dots, u_n)$ \\
-\ruleref{qnt_cnf} & Clausification of a quantified formula. \\
-\ruleref{and_pos} & $\neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k $ \\
-\ruleref{and_neg} & $ (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1 , \dots , \neg\varphi_n $ \\
-\ruleref{or_pos} & $ \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots , \varphi_n $ \\
-\ruleref{or_neg} & $ (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k $ \\
-\ruleref{xor_pos1} & $ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2) , \varphi_1 , \varphi_2 $ \\
-\ruleref{xor_pos2} & $ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2), \neg \varphi_1, \neg \varphi_2 $ \\
-\ruleref{xor_neg1} & $ \varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2 $ \\
-\ruleref{xor_neg2} & $ \varphi_1 \,\lsymb{xor}\, \varphi_2, \neg \varphi_1 , \varphi_2 $ \\
-\ruleref{implies_pos} & $ \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 $ \\
-\ruleref{implies_neg1} & $ \varphi_1 \rightarrow \varphi_2, \varphi_1 $ \\
-\ruleref{implies_neg2} & $ \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 $ \\
-\ruleref{equiv_pos1} & $\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$ \\
-\ruleref{equiv_pos2} & $\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$ \\
-\ruleref{equiv_neg1} & $\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$ \\
-\ruleref{equiv_neg2} & $\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \\
-\ruleref{ite_pos1} & $\neg (\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3) , \varphi_1 , \varphi_3$ \\
-\ruleref{ite_pos2} & $\neg (\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3) , \neg \varphi_1 , \varphi_2$ \\
-\ruleref{ite_neg1} & $\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3 , \varphi_1 , \neg \varphi_3$ \\
-\ruleref{ite_neg2} & $\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3 , \neg \varphi_1 , \neg \varphi_2$ \\
-\ruleref{connective_def} & Definition of the Boolean connectives. \\
-\ruleref{and_simplify} & Simplification of a conjunction. \\
-\ruleref{or_simplify} & Simplification of a disjunction. \\
-\ruleref{not_simplify} & Simplification of a Boolean negation. \\
-\ruleref{implies_simplify} & Simplification of an implication. \\
-\ruleref{equiv_simplify} & Simplification of an equivalence. \\
-\ruleref{bool_simplify} & Simplification of combined Boolean connectives. \\
-\ruleref{ac_simp} & Flattening of nested $\lor$ or $\land$. \\
-\ruleref{ite_simplify} & Simplification of if-then-else. \\
-\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
-\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
-\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
-\ruleref{eq_simplify} & Simplification of equality. \\
-\ruleref{div_simplify} & Simplification of division. \\
-\ruleref{prod_simplify} & Simplification of products. \\
-\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
-\ruleref{minus_simplify} & Simplification of subtractions. \\
-\ruleref{sum_simplify} & Simplification of sums. \\
-\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
-\ruleref{distinct_elim} & Elimination of the distinction predicate. \\
-\ruleref{la_rw_eq} & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \\
-\ruleref{nary_elim} & Replace $n$-ary operators with binary application. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Linear arithmetic rules.}
-\label{rule-tab:la-tauts}\\
- Rule & Description \\
- \hline
-\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
-\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
-\ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
-\ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
-\ruleref{la_tautology} & A trivial linear tautology. \\
-\ruleref{la_rw_eq} & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \\
-\ruleref{div_simplify} & Simplification of division. \\
-\ruleref{prod_simplify} & Simplification of products. \\
-\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
-\ruleref{minus_simplify} & Simplification of subtractions. \\
-\ruleref{sum_simplify} & Simplification of sums. \\
-\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Quantifier handling.}
-\label{rule-tab:quants}\\
- Rule & Description \\
- \hline
-\ruleref{forall_inst} & Instantiation of a universal variable. \\
-\ruleref{bind} & Renaming of bound variables. \\
-\ruleref{sko_ex} & Skolemization of existential variables. \\
-\ruleref{sko_forall} & Skolemization of universal variables. \\
-\ruleref{qnt_cnf} & Clausification of quantified formulas. \\
-\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
-\ruleref{onepoint} & The one-point rule. \\
-\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
-\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Skolemization rules.}
-\label{rule-tab:skos}\\
- Rule & Description \\
- \hline
-\ruleref{sko_ex} & Skolemization of existential variables. \\
-\ruleref{sko_forall} & Skolemization of universal variables. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Clausification rules. These rules can be used to perform propositional
-clausification.}
-\label{rule-tab:clausification}\\
- Rule & Description \\
- \hline
-\ruleref{and} & And elimination. \\
-\ruleref{not_or} & Elimination of a negated disjunction. \\
-\ruleref{or} & Disjunction to clause. \\
-\ruleref{not_and} & Distribution of negation over a conjunction. \\
-\ruleref{xor1} & From $\,\lsymb{xor}\, \varphi_1 \varphi_2$ to $\varphi_1, \varphi_2$. \\
-\ruleref{xor2} & From $\,\lsymb{xor}\, \varphi_1 \varphi_2$ to $\neg\varphi_1, \neg\varphi_2$. \\
-\ruleref{not_xor1} & From $\neg(\,\lsymb{xor}\, \varphi_1 \varphi_2)$ to $\varphi_1, \neg\varphi_2$. \\
-\ruleref{not_xor2} & From $\neg(\,\lsymb{xor}\, \varphi_1 \varphi_2)$ to $\neg\varphi_1, \varphi_2$. \\
-\ruleref{implies} & From $ \varphi_1\rightarrow\varphi_2 $ to $\neg\varphi_1 , \varphi_2 $. \\
-\ruleref{not_implies1} & From $\neg (\varphi_1\rightarrow\varphi_2)$ to $\varphi_1$. \\
-\ruleref{not_implies2} & From $\neg (\varphi_1\rightarrow\varphi_2)$ to $\neg\varphi_2$. \\
-\ruleref{equiv1} & From $ \varphi_1≈\varphi_2$ to $\neg\varphi_1 , \varphi_2$. \\
-\ruleref{equiv2} & From $ \varphi_1≈\varphi_2$ to $\varphi_1 , \neg\varphi_2$. \\
-\ruleref{not_equiv1} & From $\neg(\varphi_1≈\varphi_2)$ to $\varphi_1 , \varphi_2$. \\
-\ruleref{not_equiv2} & From $\neg(\varphi_1≈\varphi_2)$ to $\neg\varphi_1 , \neg\varphi_2$. \\
-\ruleref{and_pos} & $\neg (\varphi_1 \land \dots \land \varphi_n), \varphi_k$\\
-\ruleref{and_neg} & $(\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n $ \\
-\ruleref{or_pos} & $\neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
- , \varphi_n $ \\
-\ruleref{or_neg} &
-$ (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k $\\
-\ruleref{xor_pos1} &
-$ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2) , \varphi_1 , \varphi_2 $ \\
-\ruleref{xor_pos2} &
-$ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2)
-, \neg \varphi_1, \neg \varphi_2 $ \\
-\ruleref{xor_neg1} &
-$ \varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2 $ \\
-\ruleref{xor_neg2} &
-$ \varphi_1 \,\lsymb{xor}\, \varphi_2, \neg \varphi_1 , \varphi_2 $ \\
-\ruleref{implies_pos} &
-$ \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 $ \\
-\ruleref{implies_neg1} &
-$ \varphi_1 \rightarrow \varphi_2, \varphi_1 $ \\
-\ruleref{implies_neg2} &
-$ \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 $ \\
-\ruleref{equiv_pos1} &
-$\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$ \\
-\ruleref{equiv_pos2} &
-$\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$ \\
-\ruleref{equiv_neg1} &
-$\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$ \\
-\ruleref{equiv_neg2} &
-$\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \\
-\ruleref{let} & Elimination of the $\lsymb{let}$ operator. \\
-\ruleref{distinct_elim} & Elimination of the $\lsymb{distinct}$ operator. \\
-\ruleref{nary_elim} & Elimination of n-ary application of operators. \\
-\end{xltabular}
-
-\begin{xltabular}{\linewidth}{l X}
-\caption{Simplification rules. These rules represent typical operator-level
-simplifications.}
-\label{rule-tab:simplification}\\
- Rule & Description \\
- \hline
-\ruleref{connective_def} & Definition of the Boolean connectives. \\
-\ruleref{and_simplify} & Simplification of a conjunction. \\
-\ruleref{or_simplify} & Simplification of a disjunction. \\
-\ruleref{not_simplify} & Simplification of a Boolean negation. \\
-\ruleref{implies_simplify} & Simplification of an implication. \\
-\ruleref{equiv_simplify} & Simplification of an equivalence. \\
-\ruleref{bool_simplify} & Simplification of combined Boolean connectives. \\
-\ruleref{ac_simp} & Simplification of nested disjunctions and conjunctions. \\
-\ruleref{ite_simplify} & Simplification of if-then-else. \\
-\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
-\ruleref{onepoint} & The one-point rule. \\
-\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
-\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
-\ruleref{eq_simplify} & Simplification of equalities. \\
-\ruleref{div_simplify} & Simplification of division. \\
-\ruleref{prod_simplify} & Simplification of products. \\
-\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
-\ruleref{minus_simplify} & Simplification of subtractions. \\
-\ruleref{sum_simplify} & Simplification of sums. \\
-\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
-\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
-\end{xltabular}
-
-\subsection{Rule List}
-\label{sec:alethe:rules-list}
-
-\begin{RuleDescription}{assume}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi$ & \currule \\
-\end{AletheX}
- where $\varphi$ corresponds up to the orientation of equalities
- to a formula asserted in the input problem.
- \ruleparagraph{Remark.}
- This rule can not be used by the
- \inlineAlethe{(step }\dots\inlineAlethe{)} command. Instead it corresponds to the dedicated
- \inlineAlethe{(assume }\dots\inlineAlethe{)} command.
-\end{RuleDescription}
-
-\begin{RuleDescription}{hole}
-
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi$ & $(\currule\; p_1, \dots, p_n)\, [a_1, \dots, a_n]$ \\
-\end{AletheX}
-where $\varphi$ is any well-formed formula.
-
-This rule can be used to express holes in the proof. It can be used by
-solvers as a placeholder for proof steps that are not yet expressed
-by the proof rules in this document. A proof checker {\em must not}
-accept a proof as valid that contains this rule even if the checker can
-somehow check this rule. However, it is possible for checkers to have
-a dedicated status for proofs that contain this rule and are otherwise
-valid. Any other tool can accept or reject proofs that contain this rule.
-
-The premises and arguments are arbitrary, but must follow the syntax
-for premises and arguments.
-\end{RuleDescription}
-
-\begin{RuleDescription}{true}
-\begin{AletheX}
-$i$. & \ctxsep & $\top$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{false}
-\begin{AletheX}
-$i$. & \ctxsep & $\bot$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_not}
-
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\neg \neg \varphi)$, $\varphi$ & \currule \\
-\end{AletheX}
-\ruleparagraph{Remark.} This rule is useful to remove double negations from a
-clause by resolving a clause with the double negation on $\varphi$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{th_resolution}
-This rule is the resolution of two or more clauses.
-
-\begin{AletheX}
-$i_1$. & \ctxsep & $l^1_1$, $\dots$, $l^1_{k^1}$ & ($\ruleType{...}$) \\
-\aletheLine
-$i_n$. & \ctxsep & $l^n_1$, $\dots$, $l^n_{k^n}$ & ($\ruleType{...}$) \\
- $j$. & \ctxsep & $l^{r_1}_{s_1}$, $\dots$, $l^{r_m}_{s_m}$ & ($\currule\;i_1,\dots, i_n$) \\
-\end{AletheX}
-where $l^{r_1}_{s_1} , \dots , l^{r_m}_{s_m}$ are from $l^{i}_{j}$ and
-are the result of a chain of predicate resolution steps on the clauses of
-$i_1$ to $i_n$. It is possible that $m = 0$, i.e. that
-the result is the empty clause. When performing resolution steps, the
-rule implicitly merges repeated negations at the start of the formulas
-$l^{i}_{j}$. For example, the formulas $\neg\neg\neg P$ and $\neg\neg P$
-can serve as pivots during resolution. The first formula is interpreted as
-$\neg P$ and the second as just $P$ for the purpose of performing resolution
-steps.
-
-This rule is only used when the resolution step is not emitted by the SAT solver.
-See the equivalent \proofRule{resolution} rule for the rule emitted by the
-SAT solver.
-
-\ruleparagraph{Remark.} The definition given here is very general. The motivation
-for this to ensure the definition covers all possible resolution steps generated
-by the existing proof generation code in veriT. It will be restricted after
-a full review of the code. As a consequence of this checking this rule is
-theoretically NP-complete. In practice, however, the \currule-steps
-produced by {\verit} are simple. Experience with reconstructing the step in
-{\isabelle} shows that checking can done by naive decision procedures. The
-vast majority of \currule-steps are binary resolution steps.
-\end{RuleDescription}
-
-\begin{RuleDescription}{resolution}
-This rule is equivalent to the \proofRule{th_resolution} rule, but it is
-emitted by the SAT solver instead of theory reasoners. The differentiation
-serves only informational purpose.
-
-\end{RuleDescription}
-
-\begin{RuleDescription}{tautology}
-\begin{AletheX}
-$i$. & \ctxsep & $l_1$, \dots, $l_k$, \dots, $l_m$, \dots, $l_n$ & ($\dots$) \\
-$j$. & \ctxsep & $\top$ & (\currule\; $i$) \\
-\end{AletheX}
- and $l_k$, $l_m$ are such that
- \begin{align*}
- l_k &= \underbrace{\neg \dots \neg}_o \varphi \\
- l_m &= \underbrace{\neg \dots \neg}_p \varphi
- \end{align*}
- and one of $o, p$\/ is odd and the other even. Either can be $0$.
-\end{RuleDescription}
-\begin{RuleDescription}{contraction}
-\begin{AletheX}
-$i$. & \ctxsep & $l_1$, \dots, $l_n$ & ($\dots$) \\
-$j$. & \ctxsep & $l_{k_1}$, \dots, $l_{k_m}$ & (\currule\; $i$) \\
-\end{AletheX}
- where $m \leq n$ and $k_1 \dots k_m$ is a monotonic map to $1 \dots n$
- such that $l_{k_1} \dots l_{k_m}$ are pairwise distinct and
- $\{l_1, \dots, l_n\} = \{l_{k_1}, \dots, l_{k_m}\}$.
- Hence, this rule removes duplicated literals.
-\end{RuleDescription}
-
-\begin{RuleDescription}{subproof}
-The \currule{} rule completes a subproof and discharges local
-assumptions. Every subproof starts with some \proofRule{assume} steps. The
-last step of the subproof is the conclusion.
-
-\begin{AletheX}
-$i_1$. & \spctxsep & $\varphi_1$ & $\proofRule{assume}$ \\
-\aletheLine
-$i_n$. & \spctxsep & $\varphi_n$ & $\proofRule{assume}$ \\
-\aletheLineB
-$j$. & \spctxsep & $\psi$ & ($\dots$) \\
-\spsep
-k. & \ctxsep & $\neg\varphi_1$,\dots, $\neg\varphi_n$, $\psi$ & $\proofRule{subproof}$ \\
-\end{AletheX}
-
-\end{RuleDescription}
-
-\begin{RuleDescription}{la_generic}
-A step of the \currule{} rule represents a tautological clause of linear
-disequalities. It can be checked by showing that the conjunction of
-the negated disequalities is unsatisfiable. After the application of
-some strengthening rules, the resulting conjunction is unsatisfiable,
-even if integer variables are assumed to be real variables.
-
-A linear inequality is of term of the form
-\[
-\sum_{i=0}^{n}c_i\times{}t_i +
-d_1\bowtie \sum_{i=n+1}^{m} c_i\times{}t_i + d_2
-\]
-where $\bowtie\;\in \{≈, <,
->, \leq, \geq\}$, where $m\geq n$, $c_i, d_1, d_2$ are either integer or real
-constants, and for each $i$ $c_i$ and $t_i$ have the same sort. We will write
-$s_1 \bowtie s_2$.
-
-Let $l_1,\dots, l_n$ be linear inequalities and $a_1, \dots, a_n$
-rational numbers, then a {\currule} step has the form
-
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1$, \dots , $\varphi_o$ & \currule\, [$a_1$, \dots, $a_o$] \\
-\end{AletheX}
-where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
-≈ s_2$.
-
-If the current theory does not have rational numbers, then the $a_i$ are
-printed using integer division. They should, nevertheless, be interpreted
-as rational numbers. If $d_1$ or $d_2$ are $0$, they might not be printed.
-
-To check the unsatisfiability of the negation of $\varphi_1\lor \dots
-\lor \varphi_o$ one performs the following steps for each literal. For
-each $i$, let $\varphi := \varphi_i$ and $a := a_i$.
-
-\begin{enumerate}
- \item If $\varphi = s_1 > s_2$, then let $\varphi := s_1 \leq s_2$.
- If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
- If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
- If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
- the literal.
- \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
- \item Replace $\varphi$ by $\sum_{i=0}^{n}c_i\times{}t_i - \sum_{i=n+1}^{m} c_i\times{}t_i
- \bowtie d$ where $d := d_2 - d_1$.
- \item \label{la_generic:str}Now $\varphi$ has the form $s_1 \bowtie d$. If all
- variables in $s_1$ are integer sorted: replace $\bowtie d$ according to
- the table below.
- \item If $\bowtie$ is $≈$ replace $l$ by
- $\sum_{i=0}^{m}a\times{}c_i\times{}t_i ≈ a\times{}d$, otherwise replace it by
- $\sum_{i=0}^{m}|a|\times{}c_i\times{}t_i ≈ |a|\times{}d$.
-\end{enumerate}
-
-The replacements that can be performed by step~\ref{la_generic:str} above
-are
-
-\begin{tabular}{r l l}
-$\bowtie$ & If $d$ is an integer & Otherwise \\
-$>$ & $\geq d + 1$ & $\geq \lfloor d\rfloor + 1$ \\
-$\geq$ & $\geq d$ & $\geq \lfloor d\rfloor + 1$ \\
-\end{tabular}
-
-Finally, the sum of the resulting literals is trivially contradictory.
-The sum
-\[
- \sum_{k=1}^{o}\sum_{i=1}^{m^o}c_i^k*t_i^k \bowtie \sum_{k=1}^{o}d^k
-\]
-where $c_i^k$ is the constant $c_i$ of literal $l_k$, $t_i^k$ is the term
-$t_i$ of $l_k$, and $d^k$ is the constant $d$ of $l_k$. The operator
-$\bowtie$ is $≈$ if all operators are $≈$, $>$ if all are
-either $≈$ or $>$, and $\geq$ otherwise. The $a_i$ must be such
-that the sum on the left-hand side is $0$ and the right-hand side is $>0$ (or
-$\geq 0$ if $\bowtie$ is $>$).
-\end{RuleDescription}
-
-% Just like in ConTeX we can't have minted in the rule environment for some
-% reason.
-\begin{RuleExample}
-A simple \proofRule{la_generic} step in the logic \textsf{LRA} might look like this:
-
-\begin{AletheVerb}
-(step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
- :rule la_generic :args (1.0 (- 1.0)))
-\end{AletheVerb}
-
-To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
-(f\,a) ≈ (f\,b)$ (step 2). After step~3 we get $(f\,a) - (f\,b) > 0 \land
-(f\,a) - (f\,b) ≈ 0$. Since we don't have an integer sort in this logic step~4 does
-not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
-- (f\,a) + (f\,b) ≈ 0$. This sums to $0 > 0$, which is a contradiction.
-\end{RuleExample}
-
-\begin{RuleExample}
-The following \proofRule{la_generic} step is from a \textsf{QF\_UFLIA} problem:
-\begin{AletheVerb}
-(step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
- :rule la_generic :args (1 (div 1 4)))
-\end{AletheVerb}
-After normalization we get $-f_3 \geq 0 \land 4\times f_3 > 0$.
-This time step~4 applies and we can strengthen this to
-$-f_3 \geq 0 \land 4\times f_3 \geq 1$ and after multiplication we get
-$-f_3 \geq 0 \land f_3 \geq ¼$. Which sums to the contradiction
-$¼ \geq 0$.
-\end{RuleExample}
-
-\begin{RuleDescription}{lia_generic}
-This rule is a placeholder rule for integer arithmetic solving. It takes the
-same form as \proofRule{la_generic}, without the additional arguments.
-
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1$, \dots , $\varphi_o$ & (\currule) \\
-\end{AletheX}
-with $\varphi_i$ being linear inequalities. The disjunction
-$\varphi_1\lor \dots \lor \varphi_n$ is a tautology in the theory of linear
-integer arithmetic.
-
-\ruleparagraph{Remark.} Since this rule can introduce a disjunction of arbitrary
-linear integer inequalities without any additional hints, proof checking
-can be NP-hard. Hence, this rule should be avoided when possible.
-
-\end{RuleDescription}
-
-\begin{RuleDescription}{la_disequality}
-\begin{AletheX}
-$i$. & \ctxsep &
-$t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$
-& (\currule) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{la_totality}
-\begin{AletheX}
-$i$. & \ctxsep & $t_1 \leq t_2 \lor t_2 \leq t_1$ & (\currule) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{la_tautology}
-This rule is a linear arithmetic tautology which can be checked without
-sophisticated reasoning. It has either the form
-
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi$ & (\currule) \\
-\end{AletheX}
-where $\varphi$ is either a linear inequality $s_1 \bowtie s_2$
-or $\neg(s_1 \bowtie s_2)$. After performing step 1 to 3 of the process for
-checking the \proofRule{la_generic} the result is trivially unsatisfiable.
-
-The second form handles bounds on linear combinations. It is binary clause:
-
-\begin{AletheX}
-$i$. & \ctxsep &
-$\varphi_1 \lor \varphi_2$ % Checked: this is a proper disjunction not a cl
- & (\currule) \\
-\end{AletheX}
-
-It can be checked by using the procedure for \proofRule{la_generic} with
-while setting the arguments to $1$. Informally, the rule follows one of several
-cases:
-\begin{itemize}
- \item $\neg (s_1 \leq d_1) \lor s_1 \leq d_2$ where $d_1 \leq d_2$
- \item $s_1 \leq d_1 \lor \neg (s_1 \leq d_2)$ where $d_1 = d_2$
- \item $\neg (s_1 \geq d_1) \lor s_1 \geq d_2$ where $d_1 \geq d_2$
- \item $s_1 \geq d_1 \lor \neg (s_1 \geq d_2)$ where $d_1 = d_2$
- \item $\neg (s_1 \leq d_1) \lor \neg(s_1 \geq d_2)$ where $d_1 < d_2$
-\end{itemize}
-The inequalities $s_1 \bowtie d$ are are the result of applying normalization
-as for the rule \proofRule{la_generic}.
-\end{RuleDescription}
-
-\begin{RuleDescription}{bind}
- The \currule{} rule is used to rename bound variables.
-
-\begin{AletheXS}
-\aletheLineSB
-$j$. & \spctx{ $\Gamma, y_1,\dots, y_n, x_1 \mapsto y_1, \dots , x_n \mapsto y_n$}
- & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
- \spsep
-$k$. & & \ctxsep &
- $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
- & \currule{} \\
-\end{AletheXS}
- where the variables $y_1, \dots, y_n$ is not free in $\forall x_1,
- \dots, x_n.\varphi$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{sko_ex}
-The \currule{} rule skolemizes existential quantifiers.
-
-\begin{AletheXS}
-\aletheLineS
-$j$. &
-\spctx{$\Gamma, x_1 \mapsto \varepsilon_1, \dots , x_n \mapsto \varepsilon_n$}
- & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
- \spsep
-$k$. & & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
-\end{AletheXS}
-where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
-x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{i-1}\mapsto\varepsilon_{i-1}])$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{sko_forall}
-The \currule{} rule skolemizes universal quantifiers.
-
-\begin{AletheXS}
-\aletheLineS
-$j$. &
-\spctx{$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots, x_n \mapsto (\varepsilon x_n.\neg\varphi)$}
- & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
- \spsep
-$k$. & & \ctxsep & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
-\end{AletheXS}
-
-\end{RuleDescription}
-
-\begin{RuleDescription}{forall_inst}
-\begin{AletheX}
-$i$. & \ctxsep &
-$\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
- & \currule\, [$(x_{k_1}, t_{k_1})$, $\dots$, $(x_{k_n}, t_{k_n})$] \\
-\end{AletheX}
-where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_i$ and
-$k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
-\inlineAlethe{(:= xki tki)}.
-\end{RuleDescription}
-
-
-\begin{RuleDescription}{refl}
-\begin{AletheXS}
-$j$. & \ctxsep & $\Gamma$ & $t_1 ≈ t_2 $ & \currule \\
-\end{AletheXS}
-where, if $\sigma = \subst(\Gamma)$,
-the terms $t_1\sigma$ and $t_2$ are
-syntactically equal up to the orientation of equalities.
-
-\ruleparagraph{Remark.} This is the only rule that requires the application of
-the context.
-\end{RuleDescription}
-
-\begin{RuleDescription}{trans}
-\begin{AletheXS}
-$i_1$. & \ctxsep & $\Gamma$ & $t_1 ≈ t_2 $ & ($\dots$) \\
-$i_2$. & \ctxsep & $\Gamma$ & $t_2 ≈ t_3 $ & ($\dots$) \\
-\aletheLineS
-$i_n$. & \ctxsep & $\Gamma$ & $t_n ≈ t_{n+1} $ & ($\dots$) \\
-$j$. & \ctxsep & $\Gamma$ & $t_1 ≈ t_{n+1}$ & (\currule\; $i_1$, $\dots$, $i_n$) \\
-\end{AletheXS}
-\end{RuleDescription}
-
-\begin{RuleDescription}{cong}
-\begin{AletheXS}
-$i_1$. & \ctxsep & $\Gamma$ & $t_1 ≈ u_1$ & ($\dots$) \\
-$i_2$. & \ctxsep & $\Gamma$ & $t_2 ≈ u_2 $ & ($\dots$) \\
-\aletheLineS
-$i_n$. & \ctxsep & $\Gamma$ & $t_n ≈ u_n $ & ($\dots$) \\
-$j$. & \ctxsep & $\Gamma$ & $(f\,t_1\,\cdots\,t_n) ≈ (f\,u_1\,\cdots\,u_n)$ & (\currule\; $i_1$, $\dots$, $i_n$) \\
-\end{AletheXS}
-where $f$ is any $n$-ary function symbol of appropriate sort.
-\end{RuleDescription}
-
-\begin{RuleDescription}{eq_reflexive}
-\begin{AletheX}
-$i$. & \ctxsep & $t ≈ t$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{eq_transitive}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (t_1 ≈ t_2)$, $\dots$ , $\neg (t_{n-1} ≈ t_n)$,
-$t_1 ≈ t_n$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{eq_congruent}
-\begin{AletheX}
-$i$. & \ctxsep &
-$\neg (t_1 ≈ u_1)$, $\dots$ ,$\neg (t_n ≈ u_n)$,
-$(f\,t_1\, \cdots\,t_n) ≈ (f\,u_1\, \cdots\,u_n)$
- & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{eq_congruent_pred}
-\begin{AletheX}
-
-$i$. & \ctxsep &
-$\neg (t_1 ≈ u_1)$, \dots ,$\neg (t_n ≈ u_n)$,
-$(P\,t_1\, \cdots\,t_n) ≈ (P\,u_1\, \cdots\,u_n)$
- & \currule \\
-\end{AletheX}
-where $P$\, is a function symbol with co-domain sort $\lsymb{Bool}$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{qnt_cnf}
-\begin{AletheX}
-$i$. & \ctxsep &
-$\neg(\forall x_1, \dots, x_n. \varphi) \lor \forall x_{k_1}, \dots, x_{k_m}.\varphi'$
- & \currule \\
-\end{AletheX}
-
-This rule expresses clausification of a term under a universal
-quantifier. This is used by conflicting instantiation. $\varphi'$ is one of the clause
-of the clause normal form of $\varphi$. The variables $x_{k_1}, \dots, x_{k_m}$ are
-a permutation of $x_1, \dots, x_n$ plus additional variables added by prenexing
-$\varphi$. Normalization is performed in two phases. First, the negative normal form
-is formed, then the result is prenexed. The result of the first step is $\Phi(\varphi, 1)$
-where:
-
-\begin{align*}
-\Phi(\neg \varphi, 1) &:= \Phi(\varphi, 0) \\
-\Phi(\neg \varphi, 0) &:= \Phi(\varphi, 1) \\
-\Phi(\varphi_1 \lor\dots\lor\varphi_n, 1) &:= \Phi(\varphi_1, 1)\lor\dots\lor\Phi(\varphi_n, 1) \\
-\Phi(\varphi_1 \land\dots\land\varphi_n, 1) &:= \Phi(\varphi_1, 1)\land\dots\land\Phi(\varphi_n, 1) \\
-\Phi(\varphi_1 \lor\dots\lor\varphi_n, 0) &:= \Phi(\varphi_1, 0)\land\dots\land\Phi(\varphi_n, 0) \\
-\Phi(\varphi_1 \land\dots\land\varphi_n, 0) &:= \Phi(\varphi_1, 0)\lor\dots\lor\Phi(\varphi_n, 0) \\
-\Phi(\varphi_1 \rightarrow \varphi_2, 1) &:= (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land
- (\Phi(\varphi_2, 0) \lor \Phi(\varphi_1, 1)) \\
-\Phi(\varphi_1 \rightarrow \varphi_2, 0) &:= (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor
- (\Phi(\varphi_2, 1) \land \Phi(\varphi_1, 0)) \\
-\Phi(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, 1) &:=
- (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land (\Phi(\varphi_1, 1) \lor \Phi(\varphi_3, 1)) \\
-\Phi(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, 0) &:=
- (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor (\Phi(\varphi_1, 0) \land \Phi(\varphi_3, 0)) \\
-\Phi(\forall x_1, \dots, x_n. \varphi, 1) &:= \forall x_1, \dots, x_n. \Phi(\varphi, 1) \\
-\Phi(\exists x_1, \dots, x_n. \varphi, 1) &:= \exists x_1, \dots, x_n. \Phi(\varphi, 1) \\
-\Phi(\forall x_1, \dots, x_n. \varphi, 0) &:= \exists x_1, \dots, x_n. \Phi(\varphi, 0) \\
-\Phi(\exists x_1, \dots, x_n. \varphi, 0) &:= \forall x_1, \dots, x_n. \Phi(\varphi, 0) \\
-\Phi(\varphi, 1) &:= \varphi \\
-\Phi(\varphi, 0) &:= \neg\varphi
-\end{align*}
-
-\ruleparagraph{Remark.} This is a placeholder rule that combines the many steps
-done during clausification.
-\end{RuleDescription}
-
-\begin{RuleDescription}{and}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1 \land \cdots \land \varphi_n$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_k$ & (\currule\;$i$) \\
-\end{AletheX}
-and $1 \leq k \leq n$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_or}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg \varphi_k$ & (\currule\;$i$) \\
-\end{AletheX}
-and $1 \leq k \leq n$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{or}
-\begin{AletheX}
-$i$. & \ctxsep &
-$\varphi_1 \lor \cdots \lor \varphi_n$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1, \dots, \varphi_n$ & (\currule\;$i$) \\
-\end{AletheX}
-
-\ruleparagraph{Remark.} This rule deconstructs the \inlineAlethe{or} operator
-into a clause denoted by \inlineAlethe{cl}.
-\end{RuleDescription}
-
-\begin{RuleExample}
-An application of the \proofRule{or} rule.
-\begin{AletheVerb}
-(step t15 (cl (or (= a b) (not (<= a b)) (not (<= b a))))
- :rule la_disequality)
-(step t16 (cl (= a b) (not (<= a b)) (not (<= b a)))
- :rule or :premises (t15))
-\end{AletheVerb}
-\end{RuleExample}
-
-\begin{RuleDescription}{not_and}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \land \dots \land \varphi_n)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1 , \dots , \neg\varphi_n$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{xor1}
-\begin{AletheX}
-$i$. & \ctxsep & $\lsymb{xor}\,\varphi_1\,\varphi_2$
- & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1, \varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{xor2}
-\begin{AletheX}
-$i$. & \ctxsep & $\lsymb{xor}\,\varphi_1\,\varphi_2$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_xor1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg(\lsymb{xor}\,\varphi_1\,\varphi_2)$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_xor2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg(\lsymb{xor}\,\varphi_1\,\varphi_2)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1 , \varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{implies}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1\rightarrow\varphi_2$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1, \varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_implies1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1\rightarrow\varphi_2)$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_implies2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1\rightarrow\varphi_2)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv1}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1≈\varphi_2$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1, \varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv2}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1≈\varphi_2$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1, \neg\varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_equiv1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg(\varphi_1≈\varphi_2)$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1 , \varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_equiv2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg(\varphi_1≈\varphi_2)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1, \neg\varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{and_pos}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$ & \currule \\
-\end{AletheX}
-with $1 \leq k \leq n$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{and_neg}
-\begin{AletheX}
-$i$. & \ctxsep & $(\varphi_1 \land \cdots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{or_pos}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n) , \varphi_1 , \dots, \varphi_n$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{or_neg}
-\begin{AletheX}
-$i$. & \ctxsep & $(\varphi_1 \lor \cdots \lor \varphi_n), \neg \varphi_k$ & \currule \\
-\end{AletheX}
-with $1 \leq k \leq n$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{xor_pos1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1\,\lsymb{xor}\,\varphi_2) , \varphi_1 , \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{xor_pos2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1\,\lsymb{xor}\,\varphi_2), \neg \varphi_1, \neg \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{xor_neg1}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{xor_neg2}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1\,\lsymb{xor}\,\varphi_2, \neg \varphi_1, \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{implies_pos}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{implies_neg1}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1 \rightarrow \varphi_2, \varphi_1$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{implies_neg2}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1 \rightarrow \varphi_2, \neg \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv_pos1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 ≈ \varphi_2), \varphi_1, \neg \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv_pos2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 ≈ \varphi_2), \neg \varphi_1, \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv_neg1}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1 ≈ \varphi_2, \neg \varphi_1, \neg \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv_neg2}
-\begin{AletheX}
-$i$. & \ctxsep & $\varphi_1 ≈ \varphi_2, \varphi_1, \varphi_2$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite1}
-\begin{AletheX}
-$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1 , \varphi_3$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite2}
-\begin{AletheX}
-$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1, \varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite_pos1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3), \varphi_1, \varphi_3$ & (\currule) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite_pos2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg (\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3), \neg \varphi_1, \varphi_2$ & (\currule) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite_neg1}
-\begin{AletheX}
-$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, \varphi_1, \neg \varphi_3$ & (\currule) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite_neg2}
-\begin{AletheX}
-$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, \neg \varphi_1, \neg \varphi_2$ & (\currule) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_ite1}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3)$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_1, \neg\varphi_3$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_ite2}
-\begin{AletheX}
-$i$. & \ctxsep & $\neg(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{connective_def}
- This rule is used to replace connectives by their definition. It can be one
- of the following:
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
- $\varphi_1\,\lsymb{xor}\,\varphi_2 ≈
- (\neg\varphi_1 \land \varphi_2) \lor (\varphi_1 \land \neg\varphi_2)$ & \currule \\
-\end{AletheXS}
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
- $\varphi_1≈\varphi_2 ≈
- (\varphi_1 \rightarrow \varphi_2) \land (\varphi_2 \rightarrow \varphi_1)$ & \currule \\
-\end{AletheXS}
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
- $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3 ≈
- (\varphi_1 \rightarrow \varphi_2) \land (\neg\varphi_1 \rightarrow \varphi_3)$ & \currule \\
-\end{AletheXS}
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
- $\forall x_1, \dots, x_n.\,\varphi ≈ \neg(\exists x_1, \dots, x_n.\,
- \neg\varphi)$ & \currule \\
-\end{AletheXS}
-\end{RuleDescription}
-
-\begin{RuleDescription}{and_simplify}
-This rule simplifies an $\land$ term by applying equivalent
-transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\varphi_1\land \cdots\land\varphi_n ≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\psi$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $\top \land \cdots \land \top ⇒ \top$
- \item $\varphi_1 \land \cdots \land \varphi_n ⇒ \varphi_1
- \land \cdots \land \varphi_{n'} $ where the right-hand side has all
- $\top$ literals removed.
- \item $\varphi_1 \land \cdots \land \varphi_n ⇒ \varphi_1
- \land \cdots \land \varphi_{n'} $ where the right-hand side has all
- repeated literals removed.
- \item $\varphi_1 \land\cdots\land \bot\land\cdots \land \varphi_n ⇒ \bot$
- \item $\varphi_1 \land\cdots\land \varphi_i\land \cdots \land \varphi_j\land\cdots \land \varphi_n ⇒ \bot$
- and $\varphi_i$, $\varphi_j$ are such that
- \begin{align*}
- \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
- \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
- \end{align*}
- and one of $n, m$ is odd and the other even. Either can be $0$.
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{or_simplify}
-This rule simplifies an $\lor$ term by applying equivalent
-transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $(\varphi_1\lor \cdots\lor\varphi_n) ≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\psi$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $\bot \lor \cdots \lor \bot ⇒ \bot$
- \item $\varphi_1 \lor \cdots \lor \varphi_n ⇒ \varphi_1
- \lor \cdots \lor \varphi_{n'} $ where the right-hand side has all
- $\bot$ literals removed.
- \item $\varphi_1 \lor \cdots \lor \varphi_n ⇒ \varphi_1
- \lor \cdots \lor \varphi_{n'} $ where the right-hand side has all
- repeated literals removed.
- \item $\varphi_1 \lor\cdots\lor \top\lor\cdots \lor \varphi_n ⇒ \top$
- \item $\varphi_1 \lor\cdots\lor \varphi_i\lor \cdots \lor \varphi_j\lor\cdots \lor \varphi_n ⇒ \top$
- and $\varphi_i$, $\varphi_j$ are such that
- \begin{align*}
- \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
- \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
- \end{align*}
- and one of $n, m$ is odd and the other even. Either can be $0$.
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{not_simplify}
-This rule simplifies an $\neg$ term by applying equivalent
-transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\neg\varphi ≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\psi$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $\neg (\neg \varphi) ⇒ \varphi$
- \item $\neg \bot ⇒ \top$
- \item $\neg \top ⇒ \bot$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{implies_simplify}
-This rule simplifies an $\rightarrow$ term by applying equivalent
-transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\varphi_1\rightarrow \varphi_2 ≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\psi$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $\neg \varphi_1 \rightarrow \neg \varphi_2 ⇒ \varphi_2\rightarrow \varphi_1$
- \item $\bot \rightarrow \varphi ⇒ \top$
- \item $ \varphi \rightarrow \top ⇒ \top$
- \item $\top \rightarrow \varphi ⇒ \varphi$
- \item $ \varphi \rightarrow \bot ⇒ \neg \varphi$
- \item $ \varphi \rightarrow \varphi ⇒ \top$
- \item $\neg \varphi \rightarrow \varphi ⇒ \varphi$
- \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
- \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒ \varphi_1\lor \varphi_2$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{equiv_simplify}
-This rule simplifies a formula with the head symbol $≈\,: \lsymb{Bool}\,\lsymb{Bool}\,\lsymb{Bool}$
-by applying equivalent
-transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $(\varphi_1≈ \varphi_2) ≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\psi$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $(\neg \varphi_1 ≈ \neg \varphi_2) ⇒ ( \varphi_1≈ \varphi_2)$
- \item $( \varphi≈ \varphi) ⇒ \top$
- \item $( \varphi≈ \neg \varphi) ⇒ \bot$
- \item $(\neg \varphi≈ \varphi) ⇒ \bot$
- \item $(\top ≈ \varphi) ⇒ \varphi$
- \item $( \varphi ≈ \top) ⇒ \varphi$
- \item $(\bot ≈ \varphi) ⇒ \neg \varphi$
- \item $( \varphi ≈ \bot) ⇒ \neg \varphi$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{bool_simplify}
-This rule simplifies a boolean term by applying equivalent
-transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\varphi≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\psi$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $\neg(\varphi_1\rightarrow \varphi_2) ⇒ (\varphi_1 \land \neg \varphi_2)$
- \item $\neg(\varphi_1\lor \varphi_2) ⇒ (\neg \varphi_1 \land \neg \varphi_2)$
- \item $\neg(\varphi_1\land \varphi_2) ⇒ (\neg \varphi_1 \lor \neg \varphi_2)$
- \item $(\varphi_1 \rightarrow (\varphi_2\rightarrow \varphi_3)) ⇒ (\varphi_1\land \varphi_2) \rightarrow \varphi_3$
- \item $((\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2) ⇒ (\varphi_1\lor \varphi_2)$
- \item $(\varphi_1 \land (\varphi_1\rightarrow \varphi_2)) ⇒ (\varphi_1 \land \varphi_2)$
- \item $((\varphi_1\rightarrow \varphi_2) \land \varphi_1) ⇒ (\varphi_1 \land \varphi_2)$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{ac_simp}
- This rule simplifies nested occurrences of $\lor$ or $\land$:
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\psi ≈ \varphi_1 \circ\cdots\circ\varphi_n$ & \currule \\
-\end{AletheXS}
- where $\circ \in \{\lor, \land\}$ and $\psi$ is a nested application of $\circ$.
- The literals $\varphi_i$ are literals of the flattening of $\psi$ with duplicates
- removed.
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite_simplify}
- This rule simplifies an if-then-else term by applying equivalent
- transformations until fixed point\footnote{Note however that the order of the
- application is important, since the set of rules is not confluent. For
- example, the term $(\lsymb{ite} \top \; t_1 \; t_2 ≈
- t_1)$ can be simplified into both $p$ and $(\neg (\neg p))$ depending on the
- order of applications.}
- %
-It has the form
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\lsymb{ite}\,\varphi\,t_1\,t_2 ≈ u$ & \currule \\
-\end{AletheXS}
-where $u$ is the transformed term.
-
-The possible transformations are:
-\begin{itemize}
- \item $\lsymb{ite}\, \top \, t_1 \, t_2 ⇒ t_1$
- \item $\lsymb{ite}\, \bot \, t_1 \, t_2 ⇒ t_2$
- \item $\lsymb{ite}\, \psi \, t \, t ⇒ t$
- \item $\lsymb{ite}\, \neg \varphi \, t_1 \, t_2 ⇒ \lsymb{ite}\, \varphi \, t_2 \, t_1$
- \item $\lsymb{ite}\, \psi \, (\lsymb{ite}\, \psi\,t_1\,t_2)\, t_3 ⇒
- \lsymb{ite}\, \psi\, t_1\, t_3$
- \item $\lsymb{ite}\, \psi \, t_1\, (\lsymb{ite}\, \psi\,t_2\,t_3) ⇒
- \lsymb{ite}\, \psi\, t_1\, t_3$
- \item $\lsymb{ite}\, \psi \, \top\, \bot ⇒ \psi$
- \item $\lsymb{ite}\, \psi \, \bot\, \top ⇒ \neg\psi$
- \item $\lsymb{ite}\, \psi \, \top \, \varphi ⇒ \psi\lor\varphi$
- \item $\lsymb{ite}\, \psi \, \varphi\,\bot ⇒ \psi\land\varphi$
- \item $\lsymb{ite}\, \psi \, \bot\, \varphi ⇒ \neg\psi\land\varphi$
- \item $\lsymb{ite}\, \psi \, \varphi\,\top ⇒ \neg\psi\lor\varphi$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{qnt_simplify}
- This rule simplifies a $\forall$-formula with a constant predicate.
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\forall x_1, \dots, x_n. \varphi ≈ \varphi$ & \currule \\
-\end{AletheXS}
- where $\varphi$ is either $\top$ or $\bot$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{onepoint}
-The {\currule} rule is the ``one-point-rule''. That is: it eliminates quantified
-variables that can only have one value.
-
-\begin{AletheXS}
-\aletheLineS
-$j$. & \spctx{$\Gamma, x_{k_1},\dots, x_{k_m}, x_{j_1} \mapsto t_{j_1}, \dots , x_{j_o} \mapsto t_{j_o}$}
- & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
- \spsep
-$k$. & & \ctxsep & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
-\end{AletheXS}
-where $Q\in\{\forall, \exists\}$, $n = m + o$, $k_1, \dots, k_m$ and
-$j_1, \dots, j_o$ are monotone
-mappings to $1, \dots, n$, and no $x_{k_i}$ appears in $x_{j_1}, \dots, x_{j_o}$.
-
-The terms $t_{j_1}, \dots, t_{j_o}$ are the points of the variables
-$x_{j_1}, \dots, x_{j_o}$. Points are defined by equalities $x_i≈ t_i$
-with positive polarity in the term $\varphi$.
-
-\ruleparagraph{Remark.} Since an eliminated variable $x_i$ might appear free in a
-term $t_j$, it is necessary to replace $x_i$ with $t_i$ inside $t_j$. While
-this substitution is performed correctly, the proof for it is currently
-missing.
-\end{RuleDescription}
-
-\begin{RuleExample}
-An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x ≈ y
-\rightarrow (f\,x)\land (f\,y))$ look like this:
-
-\begin{AletheVerb}
-(anchor :step t3 :args ((:= y x)))
-(step t3.t1 (cl (= x y)) :rule refl)
-(step t3.t2 (cl (= (= x y) (= x x)))
- :rule cong :premises (t3.t1))
-(step t3.t3 (cl (= x y)) :rule refl)
-(step t3.t4 (cl (= (f y) (f x)))
- :rule cong :premises (t3.t3))
-(step t3.t5 (cl (= (and (f x) (f y)) (and (f x) (f x))))
- :rule cong :premises (t3.t4))
-(step t3.t6 (cl (= (=> (= x y) (and (f x) (f y)))
- (=> (= x x) (and (f x) (f x)))))
- :rule cong :premises (t3.t2 t3.t5))
-(step t3 (cl (=
- (forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
- (forall ((x S)) (=> (= x x) (and (f x) (f x))))))
- :rule qnt_simplify)
-\end{AletheVerb}
-\end{RuleExample}
-
-\begin{RuleDescription}{qnt_join}
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $Q x_1, \dots, x_n.\,(Q x_{n+1}, \dots, x_{m}.\,\varphi)
- ≈ Q x_{k_1}, \dots, x_{k_o}.\,\varphi$ & \currule \\
-\end{AletheXS}
- where $m > n$ and $Q\in\{\forall, \exists\}$. Furthermore, $k_1, \dots, k_o$ is a monotonic
- map to $1, \dots, m$ such that $x_{k_1}, \dots, x_{k_o}$ are pairwise
- distinct, and $\{x_1, \dots, x_m\} = \{x_{k_1}, \dots, x_{k_o}\}$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{qnt_rm_unused}
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $Q x_1, \dots, x_n.\,\varphi ≈ Q x_{k_1}, \dots, x_{k_m}.\,\varphi$
- & \currule \\
-\end{AletheXS}
- where $m \leq n$ and $Q\in\{\forall, \exists\}$. Furthermore, $k_1, \dots, k_m$ is
- a monotonic map to $1, \dots, n$ and if $x\in \{x_j\; |\; j \in \{1, \dots,
- n\} \land j\in\not \{k_1, \dots, k_m\}\}$ then $x$ is not free in $P$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{eq_simplify}
- This rule simplifies an $≈$ term by applying equivalent
- transformations as long as possible. Hence, the general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $(t_1≈ t_2) ≈ \varphi$ & \currule \\
-\end{AletheXS}
- where $\psi$ is the transformed term.
-
- The possible transformations are:
- \begin{itemize}
- \item $t ≈ t ⇒ \top$
- \item $(t_1 ≈ t_2) ⇒ \bot$ if $t_1$ and $t_2$ are different numeric constants.
- \item $\neg (t ≈ t) ⇒ \bot$ if $t$ is a numeric constant.
- \end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{div_simplify}
-This rule simplifies a division by applying equivalent
-transformations. The general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $(t_1\, /\, t_2) ⇒ t_3$ & \currule \\
-\end{AletheXS}
-The possible transformations are:
-\begin{itemize}
- \item $t\, /\, t ⇒ 1$
- \item $t\, /\, 1 ⇒ t$
- \item $t_1\, /\, t_2 ⇒ t_3$
- if $t_1$ and $t_2$ are constants and $t_3$ is $t_1$
- divided by $t_2$ according to the semantic of the current theory.
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{prod_simplify}
-This rule simplifies a product by applying equivalent
-transformations as long as possible. The general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $t_1\times\cdots\times t_n ≈ u$ & \currule \\
-\end{AletheXS}
-where $u$ is either a constant or a product.
-
-The possible transformations are:
-\begin{itemize}
- \item $t_1\times\cdots\times t_n ⇒ u$ where all
- $t_i$ are constants and $u$ is their product.
- \item $t_1\times\cdots\times t_n ⇒ 0$ if any
- $t_i$ is $0$.
- \item $t_1\times\cdots\times t_n ⇒
- c \times t_{k_1}\times\cdots\times t_{k_n}$ where $c$
- is the product of the constants of $t_1, \dots, t_n$ and
- $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
- with the constants removed.
- \item $t_1\times\cdots\times t_n ⇒
- t_{k_1}\times\cdots\times t_{k_n}$: same as above if $c$ is $1$.
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{unary_minus_simplify}
-This rule is either
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $- (-t) ≈ t$ & \currule \\
-\end{AletheXS}
-or
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $-t ≈ u$ & \currule \\
-\end{AletheXS}
-where $u$ is the negated numerical constant $t$.
-\end{RuleDescription}
-
-\begin{RuleDescription}{minus_simplify}
-This rule simplifies a subtraction by applying equivalent
-transformations. The general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $t_1- t_2 ≈ u$ & \currule \\
-\end{AletheXS}
-The possible transformations are:
-\begin{itemize}
- \item $t - t ⇒ 0$
- \item $t_1 - t_2 ⇒ t_3$ where $t_1$
- and $t_2$ are numerical constants and $t_3$ is $t_2$ subtracted
- from~$t_1$.
- \item $t - 0 ⇒ t$
- \item $0 - t ⇒ -t$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{sum_simplify}
-This rule simplifies a sum by applying equivalent
-transformations as long as possible. The general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $t_1+\cdots+t_n ≈ u$ & \currule \\
-\end{AletheXS}
-where $u$ is either a constant or a product.
-
-The possible transformations are:
-\begin{itemize}
- \item $t_1+\cdots+t_n ⇒ c$ where all
- $t_i$ are constants and $c$ is their sum.
- \item $t_1+\cdots+t_n ⇒
- c + t_{k_1}+\cdots+t_{k_n}$ where $c$
- is the sum of the constants of $t_1, \dots, t_n$ and
- $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
- with the constants removed.
- \item $t_1+\cdots+t_n ⇒
- t_{k_1}+\cdots+t_{k_n}$: same as above if $c$ is
- $0$.
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{comp_simplify}
-This rule simplifies a comparison by applying equivalent
-transformations as long as possible. The general form is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $t_1 \bowtie t_n ≈ \psi$ & \currule \\
-\end{AletheXS}
-where $\bowtie$ is as for the proof rule \proofRule{la_generic}, but never
-$≈$.
-
-The possible transformations are:
-\begin{itemize}
- \item $t_1 < t_2 ⇒ \varphi$ where $t_1$ and
- $t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
- strictly greater than $t_2$ and $\bot$ otherwise.
- \item $t < t ⇒ \bot$
- \item $t_1 \leq t_2 ⇒ \varphi$ where $t_1$ and
- $t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
- greater than $t_2$ or equal and $\bot$ otherwise.
- \item $t \leq t ⇒ \top$
- \item $t_1 \geq t_2 ⇒ t_2 \leq t_1$
- \item $t_1 < t_2 ⇒ \neg (t_2 \leq t_1)$
- \item $t_1 > t_2 ⇒ \neg (t_1 \leq t_2)$
-\end{itemize}
-\end{RuleDescription}
-
-\begin{RuleDescription}{let}
- This rule eliminates $\lsymb{let}$. It has the form
-
-\begin{AletheXS}
-$i_1$. & $\Gamma$ & \ctxsep & $t_{1} ≈ s_{1}$ & ($\dots$) \\
-\aletheLineS
-$i_n$. & $\Gamma$ & \ctxsep & $t_{n} ≈ s_{n}$ & ($\dots$) \\
-\aletheLineS
-$j$. & \spctx{$\Gamma, x_1 \mapsto s_1, \dots, x_n \mapsto s_n$}
- & \ctxsep & $u ≈ u'$ & ($\dots$) \\
-\spsep
-$k$. & $\Gamma$ & \ctxsep &
- $(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u) ≈ u'$
- & (\currule{}\;$i_1$, \dots, $i_n$) \\
-\end{AletheXS}
-
- The premise $i_1, \dots, i_n$ must be in the same subproof as
- the \currule{} step. If for $t_i≈ s_i$ the $t_i$ and $s_i$
- are syntactically equal, the premise
- is skipped.
-\end{RuleDescription}
-
-\begin{RuleDescription}{distinct_elim}
-This rule eliminates the $\lsymb{distinct}$ predicate. If called with one
-argument this predicate always holds:
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $(\lsymb{distinct}\, t) ≈ \top$ & \currule \\
-\end{AletheXS}
-
-If applied to terms of type $\lsymb{Bool}$ more than two terms can never be
-distinct, hence only two cases are possible:
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
-$(\lsymb{distinct}\,\varphi\,\psi) ≈ \neg (\varphi ≈ \psi)$ & \currule \\
-\end{AletheXS}
-and
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
-$(\lsymb{distinct}\,\varphi_1\,\varphi_2\,\varphi_3\,\dots) ≈ \bot$ & \currule \\
-\end{AletheXS}
-
-The general case is
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ &
-$(\lsymb{distinct}\,t_1\,\dots\, t_n) ≈
-\bigwedge_{i=1}^{n}\bigwedge_{j=i+1}^{n} t_i\;{\not≈}\;t_j$ & \currule \\
-\end{AletheXS}
-\end{RuleDescription}
-
-\begin{RuleDescription}{la_rw_eq}
-\begin{AletheX}
-$i$. & \ctxsep & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ & \currule \\
-\end{AletheX}
-\end{RuleDescription}
-
-\begin{RuleDescription}{nary_elim}
-This rule replaces $n$-ary operators with their equivalent
-application of the binary operator. It is never applied to $\land$ or $\lor$.
-
-Three cases are possible.
-If the operator $\circ$ is left associative, then the rule has the form
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\bigcirc_{i=1}^{n} t_i ≈ (\dots( t_1\circ t_2) \circ t_3)\circ \cdots t_n)$
- & \currule \\
-\end{AletheXS}
-
-If the operator $\circ$ is right associative, then the rule has the form
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\bigcirc_{i=1}^{n} t_i ≈
-( t_1 \circ \cdots \circ ( t_{n-2} \circ ( t_{n-1} \circ t_n)\dots)$ & \currule \\
-\end{AletheXS}
-
-If the operator is {\em chainable}, then it has the form
-
-\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $\bigcirc_{i=1}^{n} t_i ≈
-( t_1\circ t_2) \land ( t_2 \circ t_3) \land \cdots
-\land ( t_{n-1}\circ t_n)$ & \currule \\
-\end{AletheXS}
-\end{RuleDescription}
-
-\begin{RuleDescription}{bfun_elim}
-\begin{AletheX}
-$i$. & \ctxsep & $\psi$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi$ & (\currule\; $i$) \\
-\end{AletheX}
-
-The formula $\varphi$ is $\psi$ after boolean functions have been simplified.
-This happens in a two step process. Both steps recursively iterate over $\psi$.
-The first step expands quantified variable of type $\lsymb{Bool}$. Hence,
-$(\exists x.\,t)$ becomes $t[x\mapsto \bot]\lor t[x\mapsto \top]$ and
-$(\forall x.\,t)$ becomes $t[x\mapsto \bot]\land t[x\mapsto \top]$. If $n$ variables of sort
-$\lsymb{Bool}$ appear in a quantifier, the disjunction (conjunction) has
-$2^n$ terms. Each term replaces the variables in $t$ according
-to the bits of a number which is increased by one for each subsequent
-term starting from zero. The left-most variable corresponds to the
-least significant bit.
-
-The second step expands function argument of boolean types by introducing
-appropriate if-then-else terms. For example, consider $(f\,x\, P\, y)$ where
-$P$ is some formula. Then we replace this term by $(\lsymb{ite}\, P\,
-(f\,x\, \top\ y)\,(f\,x\, \bot\, y))$. If the argument is already the constant $\top$
-or $\bot$, it is ignored.
-\end{RuleDescription}
-
-\begin{RuleDescription}{ite_intro}
-\begin{AletheX}
-$i$. & \ctxsep & $t ≈ (t' \land u_1 \land \dots \land u_n)$ & (\currule) \\
-\end{AletheX}
-
-The term $t$ (the formula $\varphi$) contains the $\lsymb{ite}$ operator.
-Let $s_1, \dots, s_n$ be the terms starting with $\lsymb{ite}$, i.e.
-$s_i := \lsymb{ite}\,\psi_i\,r_i\,r'_i$, then $u_i$ has the form
-\[
- \lsymb{ite}\,\psi_i\,(s_i ≈ r_i)\,(s_i ≈ r'_i)
-\]
-The term $t'$ is equal to the term $t$ up to the
-reordering of equalities where one argument is an $\lsymb{ite}$
-term.
-
-\ruleparagraph{Remark.} This rule stems from the introduction of fresh
-constants for if-then-else terms inside veriT. Internally $s_i$ is a new
-constant symbol and the $\varphi$ on the right side of the equality is
-$\varphi$ with the if-then-else terms replaced by the constants. Those
-constants are unfolded during proof printing. Hence, the slightly strange
-form and the reordering of equalities.
-\end{RuleDescription}
-
-\clearpage
-\subsection{Index of Rules}
-\printindex[rules]
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index f52011c8a46cdf88b57bcd753d1638b1d18477de..c9c1b4d31ce0b323202918c8f29d9f941d4cc9d6 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1,31 +1,259 @@
-% This is the list of proof rules
-
-\begin{proof-rule}{assume}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi &\currule\\
-\end{plList}
-\end{plContainer}
-where $\varphi$ corresponds to a formula asserted in the input problem up
-to the orientation of equalities.
-\paragraph{Remark.}
-This rule can not be used by the
-$\grT{(step }\dots\grT{)}$ command. Instead it corresponds to the dedicated
-$\grT{(assume }\dots\grT{)}$ command.
-
-\end{proof-rule}
-
-\begin{proof-rule}{hole}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi &(\currule\; p_1, \dots, p_n)\; [a_1, \dots, a_n]\\
-\end{plList}
-\end{plContainer}
+This section provides a list of all proof rules supported by
+Alethe. To make this long list more accessible, the section
+first lists multiple classes of proof rules. The classes are not
+mutually exclusive: for example, the \proofRule{la_generic} rule is
+both a linear arithmetic rule and introduces a tautology.
+The number in brackets is the position of the rule in the overall list
+of proof rules.
+Table~\ref{rule-tab:special} lists rules that serve a special purpose.
+Table~\ref{rule-tab:tautologies} lists all rules that introduce
+tautologies. That is, regular rules that do not use premises.
+
+The subsequent section, starting at ref{sec:alethe:rules-list}, defines
+all rules and provides example proofs for complicated rules.
+The index of proof rules at ref{sec:alethe:rules-index} can be used
+to quickly find the definition of rules.
+
+\subsection{Classifications of the Rules}
+\label{sec:alethe:rules-overview}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Special rules.}
+\label{rule-tab:special}\\
+ Rule & Description \\
+ \hline
+ \ruleref{assume} & Repetition of an input assumption. \\
+ \ruleref{hole} & Placeholder for rules not defined here. \\
+ \ruleref{subproof} & Concludes a subproof and discharges local assumptions. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Resolution and related rules.}
+\label{rule-tab:resolution}\\
+ Rule & Description \\
+ \hline
+ \ruleref{resolution} & Chain resolution of two or more clauses. \\
+ \ruleref{th_resolution} & As \proofRule{resolution}, but used by theory solvers. \\
+ \ruleref{tautology} & Simplification of tautological clauses to $\top$. \\
+ \ruleref{contraction} & Removal of duplicated literals. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Rules introducing tautologies.}
+\label{rule-tab:tautologies}\\
+ Rule & Description \\
+ \hline
+\ruleref{true} & $\top$ \\
+\ruleref{false} & $\neg\bot$ \\
+\ruleref{not_not} & $\neg(\neg\neg\varphi), \varphi$ \\
+\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
+\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
+\ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
+\ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
+\ruleref{la_tautology} & A trivial linear tautology. \\
+\ruleref{forall_inst} & Quantifier instantiation. \\
+\ruleref{refl} & Reflexivity after applying the context. \\
+\ruleref{eq_reflexive} & $t ≈ t$ without context. \\
+\ruleref{eq_transitive} & $\neg (t_1 ≈ t_2) , \dots , \neg (t_{n-1} ≈ t_n) , t_1 ≈ t_n$ \\
+\ruleref{eq_congruent} & $\neg (t_1 ≈ u_1) , \dots , \neg (t_n ≈ u_n) , f(t_1, \dots, t_n) ≈ f(u_1, \dots, u_n)$ \\
+\ruleref{eq_congruent_pred} & $\neg (t_1 ≈ u_1) , \dots , \neg (t_n ≈ u_n) , P(t_1, \dots, t_n) ≈ P(u_1, \dots, u_n)$ \\
+\ruleref{qnt_cnf} & Clausification of a quantified formula. \\
+\ruleref{and_pos} & $\neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k $ \\
+\ruleref{and_neg} & $ (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1 , \dots , \neg\varphi_n $ \\
+\ruleref{or_pos} & $ \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots , \varphi_n $ \\
+\ruleref{or_neg} & $ (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k $ \\
+\ruleref{xor_pos1} & $ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2) , \varphi_1 , \varphi_2 $ \\
+\ruleref{xor_pos2} & $ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2), \neg \varphi_1, \neg \varphi_2 $ \\
+\ruleref{xor_neg1} & $ \varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2 $ \\
+\ruleref{xor_neg2} & $ \varphi_1 \,\lsymb{xor}\, \varphi_2, \neg \varphi_1 , \varphi_2 $ \\
+\ruleref{implies_pos} & $ \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 $ \\
+\ruleref{implies_neg1} & $ \varphi_1 \rightarrow \varphi_2, \varphi_1 $ \\
+\ruleref{implies_neg2} & $ \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 $ \\
+\ruleref{equiv_pos1} & $\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$ \\
+\ruleref{equiv_pos2} & $\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$ \\
+\ruleref{equiv_neg1} & $\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$ \\
+\ruleref{equiv_neg2} & $\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \\
+\ruleref{ite_pos1} & $\neg (\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3) , \varphi_1 , \varphi_3$ \\
+\ruleref{ite_pos2} & $\neg (\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3) , \neg \varphi_1 , \varphi_2$ \\
+\ruleref{ite_neg1} & $\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3 , \varphi_1 , \neg \varphi_3$ \\
+\ruleref{ite_neg2} & $\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3 , \neg \varphi_1 , \neg \varphi_2$ \\
+\ruleref{connective_def} & Definition of the Boolean connectives. \\
+\ruleref{and_simplify} & Simplification of a conjunction. \\
+\ruleref{or_simplify} & Simplification of a disjunction. \\
+\ruleref{not_simplify} & Simplification of a Boolean negation. \\
+\ruleref{implies_simplify} & Simplification of an implication. \\
+\ruleref{equiv_simplify} & Simplification of an equivalence. \\
+\ruleref{bool_simplify} & Simplification of combined Boolean connectives. \\
+\ruleref{ac_simp} & Flattening of nested $\lor$ or $\land$. \\
+\ruleref{ite_simplify} & Simplification of if-then-else. \\
+\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
+\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
+\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
+\ruleref{eq_simplify} & Simplification of equality. \\
+\ruleref{div_simplify} & Simplification of division. \\
+\ruleref{prod_simplify} & Simplification of products. \\
+\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
+\ruleref{minus_simplify} & Simplification of subtractions. \\
+\ruleref{sum_simplify} & Simplification of sums. \\
+\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
+\ruleref{distinct_elim} & Elimination of the distinction predicate. \\
+\ruleref{la_rw_eq} & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \\
+\ruleref{nary_elim} & Replace $n$-ary operators with binary application. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Linear arithmetic rules.}
+\label{rule-tab:la-tauts}\\
+ Rule & Description \\
+ \hline
+\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
+\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
+\ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
+\ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
+\ruleref{la_tautology} & A trivial linear tautology. \\
+\ruleref{la_rw_eq} & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \\
+\ruleref{div_simplify} & Simplification of division. \\
+\ruleref{prod_simplify} & Simplification of products. \\
+\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
+\ruleref{minus_simplify} & Simplification of subtractions. \\
+\ruleref{sum_simplify} & Simplification of sums. \\
+\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Quantifier handling.}
+\label{rule-tab:quants}\\
+ Rule & Description \\
+ \hline
+\ruleref{forall_inst} & Instantiation of a universal variable. \\
+\ruleref{bind} & Renaming of bound variables. \\
+\ruleref{sko_ex} & Skolemization of existential variables. \\
+\ruleref{sko_forall} & Skolemization of universal variables. \\
+\ruleref{qnt_cnf} & Clausification of quantified formulas. \\
+\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
+\ruleref{onepoint} & The one-point rule. \\
+\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
+\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Skolemization rules.}
+\label{rule-tab:skos}\\
+ Rule & Description \\
+ \hline
+\ruleref{sko_ex} & Skolemization of existential variables. \\
+\ruleref{sko_forall} & Skolemization of universal variables. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Clausification rules. These rules can be used to perform propositional
+clausification.}
+\label{rule-tab:clausification}\\
+ Rule & Description \\
+ \hline
+\ruleref{and} & And elimination. \\
+\ruleref{not_or} & Elimination of a negated disjunction. \\
+\ruleref{or} & Disjunction to clause. \\
+\ruleref{not_and} & Distribution of negation over a conjunction. \\
+\ruleref{xor1} & From $\,\lsymb{xor}\, \varphi_1 \varphi_2$ to $\varphi_1, \varphi_2$. \\
+\ruleref{xor2} & From $\,\lsymb{xor}\, \varphi_1 \varphi_2$ to $\neg\varphi_1, \neg\varphi_2$. \\
+\ruleref{not_xor1} & From $\neg(\,\lsymb{xor}\, \varphi_1 \varphi_2)$ to $\varphi_1, \neg\varphi_2$. \\
+\ruleref{not_xor2} & From $\neg(\,\lsymb{xor}\, \varphi_1 \varphi_2)$ to $\neg\varphi_1, \varphi_2$. \\
+\ruleref{implies} & From $ \varphi_1\rightarrow\varphi_2 $ to $\neg\varphi_1 , \varphi_2 $. \\
+\ruleref{not_implies1} & From $\neg (\varphi_1\rightarrow\varphi_2)$ to $\varphi_1$. \\
+\ruleref{not_implies2} & From $\neg (\varphi_1\rightarrow\varphi_2)$ to $\neg\varphi_2$. \\
+\ruleref{equiv1} & From $ \varphi_1≈\varphi_2$ to $\neg\varphi_1 , \varphi_2$. \\
+\ruleref{equiv2} & From $ \varphi_1≈\varphi_2$ to $\varphi_1 , \neg\varphi_2$. \\
+\ruleref{not_equiv1} & From $\neg(\varphi_1≈\varphi_2)$ to $\varphi_1 , \varphi_2$. \\
+\ruleref{not_equiv2} & From $\neg(\varphi_1≈\varphi_2)$ to $\neg\varphi_1 , \neg\varphi_2$. \\
+\ruleref{and_pos} & $\neg (\varphi_1 \land \dots \land \varphi_n), \varphi_k$\\
+\ruleref{and_neg} & $(\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n $ \\
+\ruleref{or_pos} & $\neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
+ , \varphi_n $ \\
+\ruleref{or_neg} &
+$ (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k $\\
+\ruleref{xor_pos1} &
+$ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2) , \varphi_1 , \varphi_2 $ \\
+\ruleref{xor_pos2} &
+$ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2)
+, \neg \varphi_1, \neg \varphi_2 $ \\
+\ruleref{xor_neg1} &
+$ \varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2 $ \\
+\ruleref{xor_neg2} &
+$ \varphi_1 \,\lsymb{xor}\, \varphi_2, \neg \varphi_1 , \varphi_2 $ \\
+\ruleref{implies_pos} &
+$ \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 $ \\
+\ruleref{implies_neg1} &
+$ \varphi_1 \rightarrow \varphi_2, \varphi_1 $ \\
+\ruleref{implies_neg2} &
+$ \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 $ \\
+\ruleref{equiv_pos1} &
+$\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$ \\
+\ruleref{equiv_pos2} &
+$\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$ \\
+\ruleref{equiv_neg1} &
+$\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$ \\
+\ruleref{equiv_neg2} &
+$\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \\
+\ruleref{let} & Elimination of the $\lsymb{let}$ operator. \\
+\ruleref{distinct_elim} & Elimination of the $\lsymb{distinct}$ operator. \\
+\ruleref{nary_elim} & Elimination of n-ary application of operators. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Simplification rules. These rules represent typical operator-level
+simplifications.}
+\label{rule-tab:simplification}\\
+ Rule & Description \\
+ \hline
+\ruleref{connective_def} & Definition of the Boolean connectives. \\
+\ruleref{and_simplify} & Simplification of a conjunction. \\
+\ruleref{or_simplify} & Simplification of a disjunction. \\
+\ruleref{not_simplify} & Simplification of a Boolean negation. \\
+\ruleref{implies_simplify} & Simplification of an implication. \\
+\ruleref{equiv_simplify} & Simplification of an equivalence. \\
+\ruleref{bool_simplify} & Simplification of combined Boolean connectives. \\
+\ruleref{ac_simp} & Simplification of nested disjunctions and conjunctions. \\
+\ruleref{ite_simplify} & Simplification of if-then-else. \\
+\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
+\ruleref{onepoint} & The one-point rule. \\
+\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
+\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
+\ruleref{eq_simplify} & Simplification of equalities. \\
+\ruleref{div_simplify} & Simplification of division. \\
+\ruleref{prod_simplify} & Simplification of products. \\
+\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
+\ruleref{minus_simplify} & Simplification of subtractions. \\
+\ruleref{sum_simplify} & Simplification of sums. \\
+\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
+\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
+\end{xltabular}
+
+\subsection{Rule List}
+\label{sec:alethe:rules-list}
+
+\begin{RuleDescription}{assume}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi$ & \currule \\
+\end{AletheX}
+ where $\varphi$ corresponds up to the orientation of equalities
+ to a formula asserted in the input problem.
+ \ruleparagraph{Remark.}
+ This rule can not be used by the
+ \inlineAlethe{(step }\dots\inlineAlethe{)} command. Instead it corresponds to the dedicated
+ \inlineAlethe{(assume }\dots\inlineAlethe{)} command.
+\end{RuleDescription}
+
+\begin{RuleDescription}{hole}
+
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi$ & $(\currule\; p_1, \dots, p_n)\, [a_1, \dots, a_n]$ \\
+\end{AletheX}
where $\varphi$ is any well-formed formula.
This rule can be used to express holes in the proof. It can be used by
solvers as a placeholder for proof steps that are not yet expressed
-by the proof rules in this document. A proof checker \emph{must not}
+by the proof rules in this document. A proof checker {\em must not}
accept a proof as valid that contains this rule even if the checker can
somehow check this rule. However, it is possible for checkers to have
a dedicated status for proofs that contain this rule and are otherwise
@@ -33,56 +261,44 @@ valid. Any other tool can accept or reject proofs that contain this rule.
The premises and arguments are arbitrary, but must follow the syntax
for premises and arguments.
-
-\end{proof-rule}
-
-\begin{proof-rule}{true}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \top &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{false}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg \bot &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_not}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\neg \neg \varphi) , \varphi &\currule\\
-\end{plList}
-\end{plContainer}
-
-\paragraph{Remark.} This rule is useful to remove double negations from a
-clause by resolving a clause with the double negation on \(\varphi\).
-
-\end{proof-rule}
-
-\begin{proof-rule}{th_resolution}{veriT}
+\end{RuleDescription}
+
+\begin{RuleDescription}{true}
+\begin{AletheX}
+$i$. & \ctxsep & $\top$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{false}
+\begin{AletheX}
+$i$. & \ctxsep & $\bot$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_not}
+
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\neg \neg \varphi)$, $\varphi$ & \currule \\
+\end{AletheX}
+\ruleparagraph{Remark.} This rule is useful to remove double negations from a
+clause by resolving a clause with the double negation on $\varphi$.
+\end{RuleDescription}
+
+\begin{RuleDescription}{th_resolution}
This rule is the resolution of two or more clauses.
-\begin{plContainer}
-\begin{plList}
-\proofsep& i_1.& \varphi^{1}_{1} , \dots , \varphi^{1}_{k^1} &(\dots)\\
-\plLine\\
-\proofsep& i_n.& \varphi^{n}_{1} , \dots , \varphi^{n}_{k^n} &(\dots)\\
-\proofsep& j.&
-\varphi^{r_1}_{s_1} , \dots , \varphi^{r_m}_{s_m}
-&(\currule\; i_1, \dots, i_n)\\
-\end{plList}
-\end{plContainer}
-where $\varphi^{r_1}_{s_1} , \dots , \varphi^{r_m}_{s_m}$ are from $\varphi^{i}_{j}$ and
+\begin{AletheX}
+$i_1$. & \ctxsep & $l^1_1$, $\dots$, $l^1_{k^1}$ & ($\ruleType{...}$) \\
+\aletheLine
+$i_n$. & \ctxsep & $l^n_1$, $\dots$, $l^n_{k^n}$ & ($\ruleType{...}$) \\
+ $j$. & \ctxsep & $l^{r_1}_{s_1}$, $\dots$, $l^{r_m}_{s_m}$ & ($\currule\;i_1,\dots, i_n$) \\
+\end{AletheX}
+where $l^{r_1}_{s_1} , \dots , l^{r_m}_{s_m}$ are from $l^{i}_{j}$ and
are the result of a chain of predicate resolution steps on the clauses of
$i_1$ to $i_n$. It is possible that $m = 0$, i.e. that
the result is the empty clause. When performing resolution steps, the
rule implicitly merges repeated negations at the start of the formulas
-$\varphi^{i}_{j}$. For example, the formulas $\neg\neg\neg P$ and $\neg\neg P$
+$l^{i}_{j}$. For example, the formulas $\neg\neg\neg P$ and $\neg\neg P$
can serve as pivots during resolution. The first formula is interpreted as
$\neg P$ and the second as just $P$ for the purpose of performing resolution
steps.
@@ -91,99 +307,88 @@ This rule is only used when the resolution step is not emitted by the SAT solver
See the equivalent \proofRule{resolution} rule for the rule emitted by the
SAT solver.
-\paragraph{Remark.} The definition given here is very general. The motivation
+\ruleparagraph{Remark.} The definition given here is very general. The motivation
for this to ensure the definition covers all possible resolution steps generated
by the existing proof generation code in veriT. It will be restricted after
a full review of the code. As a consequence of this checking this rule is
theoretically NP-complete. In practice, however, the \currule-steps
-produced by veriT are simple. Experience with reconstructing the step in
-Isabelle/HOL shows that checking can done by naive decision procedures. The
+produced by {\verit} are simple. Experience with reconstructing the step in
+{\isabelle} shows that checking can done by naive decision procedures. The
vast majority of \currule-steps are binary resolution steps.
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{resolution}{veriT}
+\begin{RuleDescription}{resolution}
This rule is equivalent to the \proofRule{th_resolution} rule, but it is
emitted by the SAT solver instead of theory reasoners. The differentiation
serves only informational purpose.
-\end{proof-rule}
-
-\begin{proof-rule}{tautology}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.&
- \varphi_1 , \dots , \varphi_k , \dots , \varphi_l ,\dots , \varphi_n
- &(\dots)\\
- \proofsep& j.& \top &(\currule\; i)\\
- \end{plList}
- \end{plContainer}
- and $\varphi_i$, $\varphi_j$ are such that
+\end{RuleDescription}
+
+\begin{RuleDescription}{tautology}
+\begin{AletheX}
+$i$. & \ctxsep & $l_1$, \dots, $l_k$, \dots, $l_m$, \dots, $l_n$ & ($\dots$) \\
+$j$. & \ctxsep & $\top$ & (\currule\; $i$) \\
+\end{AletheX}
+ and $l_k$, $l_m$ are such that
\begin{align*}
- \varphi_k &= \underbrace{\neg \dots \neg}_n \psi \\
- \varphi_l &= \underbrace{\neg \dots \neg}_m \psi
+ l_k &= \underbrace{\neg \dots \neg}_o \varphi \\
+ l_m &= \underbrace{\neg \dots \neg}_p \varphi
\end{align*}
- and one of $n, m$ is odd and the other even. Either can be $0$.
-\end{proof-rule}
-
-\begin{proof-rule}{contraction}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.& \varphi_1 , \dots , \varphi_n &(\dots)\\
- \proofsep& j.& \varphi_{k_1} , \dots , \varphi_{k_m}
- &(\currule\; i)\\
- \end{plList}
- \end{plContainer}
+ and one of $o, p$\/ is odd and the other even. Either can be $0$.
+\end{RuleDescription}
+\begin{RuleDescription}{contraction}
+\begin{AletheX}
+$i$. & \ctxsep & $l_1$, \dots, $l_n$ & ($\dots$) \\
+$j$. & \ctxsep & $l_{k_1}$, \dots, $l_{k_m}$ & (\currule\; $i$) \\
+\end{AletheX}
where $m \leq n$ and $k_1 \dots k_m$ is a monotonic map to $1 \dots n$
- such that $\varphi_{k_1} \dots \varphi_{k_m}$ are pairwise distinct and
- $\{\varphi_1, \dots, \varphi_n\} = \{\varphi_{k_1}, \dots, \varphi_{k_m}\}$.
+ such that $l_{k_1} \dots l_{k_m}$ are pairwise distinct and
+ $\{l_1, \dots, l_n\} = \{l_{k_1}, \dots, l_{k_m}\}$.
Hence, this rule removes duplicated literals.
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{subproof}{veriT}
+\begin{RuleDescription}{subproof}
The \currule{} rule completes a subproof and discharges local
-assumptions. Every subproof starts with some \ruleType{assume} steps. The
+assumptions. Every subproof starts with some \proofRule{assume} steps. The
last step of the subproof is the conclusion.
-\begin{plContainer}
-\begin{plSubList}
-\proofsep& i_1.& \psi_1 &\proofRule{assume}\\
-\plLine\\
-\proofsep& i_n.& \psi_n &\proofRule{assume}\\
-\plLine\\
-\proofsep& j.& \varphi &(\dots)\\
-\end{plSubList}
-\begin{plList}
-\proofsep& k.& \neg\psi_1 , \dots , \neg \psi_n ,\varphi &\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheX}
+$i_1$. & \spctxsep & $\varphi_1$ & $\proofRule{assume}$ \\
+\aletheLine
+$i_n$. & \spctxsep & $\varphi_n$ & $\proofRule{assume}$ \\
+\aletheLineB
+$j$. & \spctxsep & $\psi$ & ($\dots$) \\
+\spsep
+k. & \ctxsep & $\neg\varphi_1$,\dots, $\neg\varphi_n$, $\psi$ & $\proofRule{subproof}$ \\
+\end{AletheX}
-\end{proof-rule}
+\end{RuleDescription}
-
-\begin{proof-rule}{la_generic}{veriT}
-A step of the $\currule$ rule represents a tautological clause of linear
+\begin{RuleDescription}{la_generic}
+A step of the \currule{} rule represents a tautological clause of linear
disequalities. It can be checked by showing that the conjunction of
the negated disequalities is unsatisfiable. After the application of
some strengthening rules, the resulting conjunction is unsatisfiable,
even if integer variables are assumed to be real variables.
-A linear inequality is of term of the form $\sum_{i=0}^{n}c_i\times{}t_i +
-d_1\bowtie \sum_{i=n+1}^{m} c_i\times{}t_i + d_2$ where $\bowtie\;\in \{\simeq, <,
+A linear inequality is of term of the form
+\[
+\sum_{i=0}^{n}c_i\times{}t_i +
+d_1\bowtie \sum_{i=n+1}^{m} c_i\times{}t_i + d_2
+\]
+where $\bowtie\;\in \{≈, <,
>, \leq, \geq\}$, where $m\geq n$, $c_i, d_1, d_2$ are either integer or real
constants, and for each $i$ $c_i$ and $t_i$ have the same sort. We will write
$s_1 \bowtie s_2$.
Let $l_1,\dots, l_n$ be linear inequalities and $a_1, \dots, a_n$
-rational numbers, then a $\currule$ step has the form
-
-\begin{plListEq}
-\proofsep& i.&
-\varphi_1, \dots , \varphi_o
-&\currule\;[a_1, \dots, a_o]\\
-\end{plListEq}
+rational numbers, then a {\currule} step has the form
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1$, \dots , $\varphi_o$ & \currule\, [$a_1$, \dots, $a_o$] \\
+\end{AletheX}
where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
-\simeq s_2$.
+≈ s_2$.
If the current theory does not have rational numbers, then the $a_i$ are
printed using integer division. They should, nevertheless, be interpreted
@@ -195,137 +400,122 @@ each $i$, let $\varphi := \varphi_i$ and $a := a_i$.
\begin{enumerate}
\item If $\varphi = s_1 > s_2$, then let $\varphi := s_1 \leq s_2$.
- If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
- If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
- If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
- the literal.
- \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
+ If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
+ If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
+ If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
+ the literal.
+ \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
\item Replace $\varphi$ by $\sum_{i=0}^{n}c_i\times{}t_i - \sum_{i=n+1}^{m} c_i\times{}t_i
\bowtie d$ where $d := d_2 - d_1$.
- \item Now $\varphi$ has the form $s_1 \bowtie d$. If all
+ \item \label{la_generic:str}Now $\varphi$ has the form $s_1 \bowtie d$. If all
variables in $s_1$ are integer sorted: replace $\bowtie d$ according to
- table~\ref{tb:lageneric}.
- \item If $\bowtie$ is $\simeq$ replace $l$ by
- $\sum_{i=0}^{m}a\times{}c_i\times{}t_i \simeq a\times{}d$, otherwise replace it by
- $\sum_{i=0}^{m}|a|\times{}c_i\times{}t_i \simeq |a|\times{}d$.
+ the table below.
+ \item If $\bowtie$ is $≈$ replace $l$ by
+ $\sum_{i=0}^{m}a\times{}c_i\times{}t_i ≈ a\times{}d$, otherwise replace it by
+ $\sum_{i=0}^{m}|a|\times{}c_i\times{}t_i ≈ |a|\times{}d$.
\end{enumerate}
-\begin{table}[h!]
-\centering
-\begin{tabular}{c|l l}
-$\bowtie$ & If $d$ is an integer & Otherwise \\
-\hline
-$>$ & $\geq d + 1$ & $\geq \lfloor d\rfloor + 1$ \\
-$\geq$ & $\geq d$ & $\geq \lfloor d\rfloor + 1$ \\
+The replacements that can be performed by step~\ref{la_generic:str} above
+are
+
+\begin{tabular}{r l l}
+$\bowtie$ & If $d$ is an integer & Otherwise \\
+$>$ & $\geq d + 1$ & $\geq \lfloor d\rfloor + 1$ \\
+$\geq$ & $\geq d$ & $\geq \lfloor d\rfloor + 1$ \\
\end{tabular}
-\caption{Strengthening rules for \texttt{la\_generic}.}
-\label{tb:lageneric}
-\end{table}
Finally, the sum of the resulting literals is trivially contradictory.
The sum
-\begin{equation*}
+\[
\sum_{k=1}^{o}\sum_{i=1}^{m^o}c_i^k*t_i^k \bowtie \sum_{k=1}^{o}d^k
-\end{equation*}
+\]
where $c_i^k$ is the constant $c_i$ of literal $l_k$, $t_i^k$ is the term
$t_i$ of $l_k$, and $d^k$ is the constant $d$ of $l_k$. The operator
-$\bowtie$ is $\simeq$ if all operators are $\simeq$, $>$ if all are
-either $\simeq$ or $>$, and $\geq$ otherwise. The $a_i$ must be such
+$\bowtie$ is $≈$ if all operators are $≈$, $>$ if all are
+either $≈$ or $>$, and $\geq$ otherwise. The $a_i$ must be such
that the sum on the left-hand side is $0$ and the right-hand side is $>0$ (or
$\geq 0$ if $\bowtie$ is $>$).
+\end{RuleDescription}
+
+% Just like in ConTeX we can't have minted in the rule environment for some
+% reason.
+\begin{RuleExample}
+A simple \proofRule{la_generic} step in the logic \textsf{LRA} might look like this:
-\begin{rule-example}
-A simple $\currule$ step in the logic \texttt{LRA} might look like this:
-\begin{minted}{smtlib2.py -x}
+\begin{AletheVerb}
(step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
:rule la_generic :args (1.0 (- 1.0)))
-\end{minted}
-To verify this we have to check the insatisfiability of $f(a) > f(b) \land
-f(a) = f(b)$ (Step 2). After step 3 we get $f(a) - f(b) > 0 \land
-f(a) - f(b) = 0$. Since we don't have an integer sort in this logic step~4 does
-not apply. Finally, after step~5 the conjunction is $f(a) - f(b) > 0 \land
-- f(a) + f(b) = 0$. This sums to $0 > 0$, which is a contradiction.
-\end{rule-example}
-
-\begin{rule-example}
-The following $\currule$ step is from a \texttt{QF_UFLIA} problem:
-\begin{minted}{smtlib2.py -x}
+\end{AletheVerb}
+
+To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
+(f\,a) ≈ (f\,b)$ (step 2). After step~3 we get $(f\,a) - (f\,b) > 0 \land
+(f\,a) - (f\,b) ≈ 0$. Since we don't have an integer sort in this logic step~4 does
+not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
+- (f\,a) + (f\,b) ≈ 0$. This sums to $0 > 0$, which is a contradiction.
+\end{RuleExample}
+
+\begin{RuleExample}
+The following \proofRule{la_generic} step is from a \textsf{QF\_UFLIA} problem:
+\begin{AletheVerb}
(step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
:rule la_generic :args (1 (div 1 4)))
-\end{minted}
+\end{AletheVerb}
After normalization we get $-f_3 \geq 0 \land 4\times f_3 > 0$.
This time step~4 applies and we can strengthen this to
$-f_3 \geq 0 \land 4\times f_3 \geq 1$ and after multiplication we get
-$-f_3 \geq 0 \land f_3 \geq \frac{1}{4}$. Which sums to the contradiction
-$\frac{1}{4} \geq 0$.
-\end{rule-example}
+$-f_3 \geq 0 \land f_3 \geq ¼$. Which sums to the contradiction
+$¼ \geq 0$.
+\end{RuleExample}
-\end{proof-rule}
-
-\begin{proof-rule}{lia_generic}{veriT}
+\begin{RuleDescription}{lia_generic}
This rule is a placeholder rule for integer arithmetic solving. It takes the
-same form as \texttt{la\_generic}, without the additional arguments.
-
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\varphi_1, \dots , \varphi_n
-&\currule\\
-\end{plList}
-\end{plContainer}
+same form as \proofRule{la_generic}, without the additional arguments.
+
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1$, \dots , $\varphi_o$ & (\currule) \\
+\end{AletheX}
with $\varphi_i$ being linear inequalities. The disjunction
$\varphi_1\lor \dots \lor \varphi_n$ is a tautology in the theory of linear
integer arithmetic.
-\paragraph{Remark.} Since this rule can introduce a disjunction of arbitrary
+\ruleparagraph{Remark.} Since this rule can introduce a disjunction of arbitrary
linear integer inequalities without any additional hints, proof checking
can be NP-hard. Hence, this rule should be avoided when possible.
-\end{proof-rule}
-
-\begin{proof-rule}{la_disequality}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-t_1 \simeq t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{la_totality}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-t_1 \leq t_2 \lor t_2 \leq t_1
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{la_tautology}{veriT}
+\end{RuleDescription}
+
+\begin{RuleDescription}{la_disequality}
+\begin{AletheX}
+$i$. & \ctxsep &
+$t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$
+& (\currule) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{la_totality}
+\begin{AletheX}
+$i$. & \ctxsep & $t_1 \leq t_2 \lor t_2 \leq t_1$ & (\currule) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{la_tautology}
This rule is a linear arithmetic tautology which can be checked without
sophisticated reasoning. It has either the form
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\varphi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi$ & (\currule) \\
+\end{AletheX}
where $\varphi$ is either a linear inequality $s_1 \bowtie s_2$
or $\neg(s_1 \bowtie s_2)$. After performing step 1 to 3 of the process for
checking the \proofRule{la_generic} the result is trivially unsatisfiable.
The second form handles bounds on linear combinations. It is binary clause:
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\varphi_1 \lor \varphi_2 % Checked: this is a proper disjunction not a cl
-&\currule\\
-\end{plList}
-\end{plContainer}
+
+\begin{AletheX}
+$i$. & \ctxsep &
+$\varphi_1 \lor \varphi_2$ % Checked: this is a proper disjunction not a cl
+ & (\currule) \\
+\end{AletheX}
It can be checked by using the procedure for \proofRule{la_generic} with
while setting the arguments to $1$. Informally, the rule follows one of several
@@ -339,225 +529,138 @@ cases:
\end{itemize}
The inequalities $s_1 \bowtie d$ are are the result of applying normalization
as for the rule \proofRule{la_generic}.
+\end{RuleDescription}
-\end{proof-rule}
-
-\begin{proof-rule}{bind}{veriT}
+\begin{RuleDescription}{bind}
The \currule{} rule is used to rename bound variables.
- \begin{plContainer}
- \begin{plSubList}
- \plLine\\
- \Gamma, y_1,\dots, y_n, x_1 \mapsto y_1, \dots , x_n \mapsto y_n,
- \proofsep& j.& \varphi \leftrightarrow \varphi' &(\dots)\\
- \end{plSubList}
- \begin{plList}
- \Gamma \proofsep& k.&
- \forall x_1, \dots, x_n.\varphi \leftrightarrow \forall y_1, \dots, y_n. \varphi' &\currule\\
- \end{plList}
- \end{plContainer}
+\begin{AletheXS}
+\aletheLineSB
+$j$. & \spctx{ $\Gamma, y_1,\dots, y_n, x_1 \mapsto y_1, \dots , x_n \mapsto y_n$}
+ & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
+ \spsep
+$k$. & & \ctxsep &
+ $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
+ & \currule{} \\
+\end{AletheXS}
where the variables $y_1, \dots, y_n$ is not free in $\forall x_1,
\dots, x_n.\varphi$.
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{sko_ex}{veriT}
+\begin{RuleDescription}{sko_ex}
The \currule{} rule skolemizes existential quantifiers.
-\begin{plContainer}
-\begin{plSubList}
-\plLine\\
-\Gamma, x_1 \mapsto \varepsilon_1, \dots , x_n \mapsto \varepsilon_n
-\proofsep& j.&\varphi \leftrightarrow \psi &(\dots)\\
-\end{plSubList}
-\begin{plList}
-\Gamma \proofsep& k.&
-\exists x_1, \dots, x_n.\varphi \leftrightarrow \psi &\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+\aletheLineS
+$j$. &
+\spctx{$\Gamma, x_1 \mapsto \varepsilon_1, \dots , x_n \mapsto \varepsilon_n$}
+ & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
+ \spsep
+$k$. & & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
+\end{AletheXS}
where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{i-1}\mapsto\varepsilon_{i-1}])$.
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{sko_forall}{veriT}
+\begin{RuleDescription}{sko_forall}
The \currule{} rule skolemizes universal quantifiers.
-\begin{plContainer}
-\begin{center}
-\parbox{\textwidth}{
-\begin{plSubList}
-\plLine\\
-\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots, x_n \mapsto (\varepsilon x_n.\neg\varphi)
-\proofsep& j.&
-\varphi \leftrightarrow \psi
-&(\dots)\\
-\end{plSubList}
-\begin{plList}
-\Gamma \proofsep& k.&
-\forall x_1, \dots, x_n.\varphi \leftrightarrow \psi &\currule\\
-\end{plList}}
-\end{center}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{forall_inst}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]
-&\currule\; [(x_{k_1}, t_{k_1}), \dots, (x_{k_n}, t_{k_n})]\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+\aletheLineS
+$j$. &
+\spctx{$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots, x_n \mapsto (\varepsilon x_n.\neg\varphi)$}
+ & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
+ \spsep
+$k$. & & \ctxsep & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
+\end{AletheXS}
+
+\end{RuleDescription}
+
+\begin{RuleDescription}{forall_inst}
+\begin{AletheX}
+$i$. & \ctxsep &
+$\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
+ & \currule\, [$(x_{k_1}, t_{k_1})$, $\dots$, $(x_{k_n}, t_{k_n})$] \\
+\end{AletheX}
where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_i$ and
$k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
-\smtinline{(:= xki tki)}.
-
-\paragraph{Remark.} A rule similar to the \proofRule{let} rule would be
-more appropriate. The resulting proof would be more fine grained and this
-would also be an opportunity to provide a proof for the clausification
-as currently done by \proofRule{qnt_cnf}.
-
-\end{proof-rule}
-
-\begin{proof-rule}{refl}{veriT}
-Either
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep& j.& t_1 \simeq t_2 &\currule\\
-\end{plList}
-\end{plContainer}
-or
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep& j.& \varphi_1 \leftrightarrow \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-
-where, if $\sigma = \operatorname{subst}(\Gamma)$,
-the terms $t_1\sigma$ and $t_2$ (the formulas $\varphi_1\sigma$ and $\varphi_2$) are
+\inlineAlethe{(:= xki tki)}.
+\end{RuleDescription}
+
+
+\begin{RuleDescription}{refl}
+\begin{AletheXS}
+$j$. & \ctxsep & $\Gamma$ & $t_1 ≈ t_2 $ & \currule \\
+\end{AletheXS}
+where, if $\sigma = \subst(\Gamma)$,
+the terms $t_1\sigma$ and $t_2$ are
syntactically equal up to the orientation of equalities.
-\paragraph{Remark.} This is the only rule that requires the application of
+\ruleparagraph{Remark.} This is the only rule that requires the application of
the context.
-\end{proof-rule}
-
-\begin{proof-rule}{trans}{veriT}
-Either
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep& i_1.& t_1 \simeq t_2 &(\dots)\\
-\Gamma\proofsep& i_2.& t_2 \simeq t_3 &(\dots)\\
- \plLine\\
-\Gamma\proofsep& i_n.& t_n \simeq t_{n+1} &(\dots)\\
-\Gamma\proofsep& j.& t_1 \simeq t_{n+1} &(\currule\; i_1, \dots, i_n)\\
-\end{plList}
-\end{plContainer}
-or
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep& i_1.& \varphi_1 \leftrightarrow \varphi_2 &(\dots)\\
-\Gamma\proofsep& i_2.& \varphi_2 \leftrightarrow \varphi_3 &(\dots)\\
- \plLine\\
-\Gamma\proofsep& i_n.& \varphi_n \leftrightarrow \varphi_{n+1} &(\dots)\\
-\Gamma\proofsep& j.& \varphi_1 \leftrightarrow \varphi_{n+1} &(\currule\; i_1,\dots, i_n)\\
-\end{plList}
-\end{plContainer}
-
-\begin{comment}{Mathias Fleury} The \proofRule{trans} rules comes in three
-flavors that can be distinguished by the attribute: \begin{description}
-\item[ordered and oriented] the equalities are given in the correct order
-and are oriented in the right direction; \item[ordered and unoriented]
-the equalities are given in the correct order, but
- the equalitis like ``\(t_1\simeq t_2\)'' can be used as ``\(t_1\simeq
- t_2\)'' or ``\(t_2\simeq t_1\)'';
-\item[unordered and unoriented] the equalities are not ordered either.
-\end{description}
-\end{comment}
-
-\end{proof-rule}
-
-\begin{proof-rule}{cong}{veriT}
-Either
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep& i_1.& t_1 \simeq u_1 &(\dots)\\
- \plLine\\
-\Gamma\proofsep& i_n.& t_n \simeq u_n &(\dots)\\
-\Gamma\proofsep& j.& \operatorname{f}(t_1, \dots, t_n) \simeq
-\operatorname{f}(u_1, \dots, u_n) &(\currule\;i_1, \dots, i_n)\\
-\end{plList}
-\end{plContainer}
-where $\operatorname{f}$ is an $n$-ary function symbol,
-or
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep& i_1.& \varphi_1 \simeq \psi_1 &(\dots)\\
- \plLine\\
-\Gamma\proofsep& i_n.& \varphi_n \simeq \psi_n &(\dots)\\
-\Gamma\proofsep& j.& \operatorname{P}(\varphi_1, \dots, \varphi_n) \leftrightarrow
-\operatorname{P}(\psi_1, \dots, \psi_n) &(\currule\;i_1, \dots, i_n)\\
-\end{plList}
-\end{plContainer}
-where $\operatorname{P}$ is an $n$-ary predicate symbol.
-\end{proof-rule}
-
-
-\begin{proof-rule}{eq_reflexive}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-t \simeq t
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{eq_transitive}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg (t_1 \simeq t_2) , \dots , \neg (t_{n-1} \simeq t_n) ,
-t_1 \simeq t_n
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{eq_congruent}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg (t_1 \simeq u_1) , \dots , \neg (t_n \simeq u_n) ,
-f(t_1, \dots, t_n) \simeq f(u_1, \dots, u_n)
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-% TODO: why does this exist?
-\begin{proof-rule}{eq_congruent_pred}{veriT}
-%\begin{compactproof}
-%\begingroup\abovedisplayskip=0pt \belowdisplayskip=0pt%
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg (t_1 \simeq u_1) , \dots , \neg (t_n \simeq u_n) ,
-\neg (P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n))
-&\currule\\
-\end{plList}
-\end{plContainer}
-%\endgroup
-%\end{compactproof}
-%
-\end{proof-rule}
-
-\begin{proof-rule}{qnt_cnf}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg(\forall x_1, \dots, x_n. \varphi) \lor \forall x_{k_1}, \dots, x_{k_m}.\varphi'
-&\currule\\
-\end{plList}
-\end{plContainer}
+\end{RuleDescription}
+
+\begin{RuleDescription}{trans}
+\begin{AletheXS}
+$i_1$. & \ctxsep & $\Gamma$ & $t_1 ≈ t_2 $ & ($\dots$) \\
+$i_2$. & \ctxsep & $\Gamma$ & $t_2 ≈ t_3 $ & ($\dots$) \\
+\aletheLineS
+$i_n$. & \ctxsep & $\Gamma$ & $t_n ≈ t_{n+1} $ & ($\dots$) \\
+$j$. & \ctxsep & $\Gamma$ & $t_1 ≈ t_{n+1}$ & (\currule\; $i_1$, $\dots$, $i_n$) \\
+\end{AletheXS}
+\end{RuleDescription}
+
+\begin{RuleDescription}{cong}
+\begin{AletheXS}
+$i_1$. & \ctxsep & $\Gamma$ & $t_1 ≈ u_1$ & ($\dots$) \\
+$i_2$. & \ctxsep & $\Gamma$ & $t_2 ≈ u_2 $ & ($\dots$) \\
+\aletheLineS
+$i_n$. & \ctxsep & $\Gamma$ & $t_n ≈ u_n $ & ($\dots$) \\
+$j$. & \ctxsep & $\Gamma$ & $(f\,t_1\,\cdots\,t_n) ≈ (f\,u_1\,\cdots\,u_n)$ & (\currule\; $i_1$, $\dots$, $i_n$) \\
+\end{AletheXS}
+where $f$ is any $n$-ary function symbol of appropriate sort.
+\end{RuleDescription}
+
+\begin{RuleDescription}{eq_reflexive}
+\begin{AletheX}
+$i$. & \ctxsep & $t ≈ t$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{eq_transitive}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (t_1 ≈ t_2)$, $\dots$ , $\neg (t_{n-1} ≈ t_n)$,
+$t_1 ≈ t_n$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{eq_congruent}
+\begin{AletheX}
+$i$. & \ctxsep &
+$\neg (t_1 ≈ u_1)$, $\dots$ ,$\neg (t_n ≈ u_n)$,
+$(f\,t_1\, \cdots\,t_n) ≈ (f\,u_1\, \cdots\,u_n)$
+ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{eq_congruent_pred}
+\begin{AletheX}
+
+$i$. & \ctxsep &
+$\neg (t_1 ≈ u_1)$, \dots ,$\neg (t_n ≈ u_n)$,
+$(P\,t_1\, \cdots\,t_n) ≈ (P\,u_1\, \cdots\,u_n)$
+ & \currule \\
+\end{AletheX}
+where $P$\, is a function symbol with co-domain sort $\lsymb{Bool}$.
+\end{RuleDescription}
+
+\begin{RuleDescription}{qnt_cnf}
+\begin{AletheX}
+$i$. & \ctxsep &
+$\neg(\forall x_1, \dots, x_n. \varphi) \lor \forall x_{k_1}, \dots, x_{k_m}.\varphi'$
+ & \currule \\
+\end{AletheX}
+
This rule expresses clausification of a term under a universal
quantifier. This is used by conflicting instantiation. $\varphi'$ is one of the clause
of the clause normal form of $\varphi$. The variables $x_{k_1}, \dots, x_{k_m}$ are
@@ -566,467 +669,347 @@ $\varphi$. Normalization is performed in two phases. First, the negative normal
is formed, then the result is prenexed. The result of the first step is $\Phi(\varphi, 1)$
where:
-{\allowdisplaybreaks
- \begin{align*}
- \Phi(\neg \varphi, 1) &:= \Phi(\varphi, 0)\\
- \Phi(\neg \varphi, 0) &:= \Phi(\varphi, 1)\\
- \Phi(\varphi_1 \lor\dots\lor\varphi_n, 1) &:= \Phi(\varphi_1, 1)\lor\dots\lor\Phi(\varphi_n, 1)\\
- \Phi(\varphi_1 \land\dots\land\varphi_n, 1) &:= \Phi(\varphi_1, 1)\land\dots\land\Phi(\varphi_n, 1)\\
- \Phi(\varphi_1 \lor\dots\lor\varphi_n, 0) &:= \Phi(\varphi_1, 0)\land\dots\land\Phi(\varphi_n, 0)\\
- \Phi(\varphi_1 \land\dots\land\varphi_n, 0) &:= \Phi(\varphi_1, 0)\lor\dots\lor\Phi(\varphi_n, 0)\\
- \Phi(\varphi_1 \rightarrow \varphi_2, 1) &:= (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land
- (\Phi(\varphi_2, 0) \lor \Phi(\varphi_1, 1))\\
- \Phi(\varphi_1 \rightarrow \varphi_2, 0) &:= (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor
- (\Phi(\varphi_2, 1) \land \Phi(\varphi_1, 0))\\
- \Phi(\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3, 1) &:=
- (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land (\Phi(\varphi_1, 1) \lor \Phi(\varphi_3, 1))\\
- \Phi(\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3, 0) &:=
- (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor (\Phi(\varphi_1, 0) \land \Phi(\varphi_3, 0))\\
- \Phi(\forall x_1, \dots, x_n. \varphi, 1) &:= \forall x_1, \dots, x_n. \Phi(\varphi, 1)\\
- \Phi(\exists x_1, \dots, x_n. \varphi, 1) &:= \exists x_1, \dots, x_n. \Phi(\varphi, 1)\\
- \Phi(\forall x_1, \dots, x_n. \varphi, 0) &:= \exists x_1, \dots, x_n. \Phi(\varphi, 0)\\
- \Phi(\exists x_1, \dots, x_n. \varphi, 0) &:= \forall x_1, \dots, x_n. \Phi(\varphi, 0)\\
- \Phi(\varphi, 1) &:= \varphi\\
- \Phi(\varphi, 0) &:= \neg\varphi\\
- \end{align*}
-}
-
-\paragraph{Remark.} This is a placeholder rule that combines the many steps
+\begin{align*}
+\Phi(\neg \varphi, 1) &:= \Phi(\varphi, 0) \\
+\Phi(\neg \varphi, 0) &:= \Phi(\varphi, 1) \\
+\Phi(\varphi_1 \lor\dots\lor\varphi_n, 1) &:= \Phi(\varphi_1, 1)\lor\dots\lor\Phi(\varphi_n, 1) \\
+\Phi(\varphi_1 \land\dots\land\varphi_n, 1) &:= \Phi(\varphi_1, 1)\land\dots\land\Phi(\varphi_n, 1) \\
+\Phi(\varphi_1 \lor\dots\lor\varphi_n, 0) &:= \Phi(\varphi_1, 0)\land\dots\land\Phi(\varphi_n, 0) \\
+\Phi(\varphi_1 \land\dots\land\varphi_n, 0) &:= \Phi(\varphi_1, 0)\lor\dots\lor\Phi(\varphi_n, 0) \\
+\Phi(\varphi_1 \rightarrow \varphi_2, 1) &:= (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land
+ (\Phi(\varphi_2, 0) \lor \Phi(\varphi_1, 1)) \\
+\Phi(\varphi_1 \rightarrow \varphi_2, 0) &:= (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor
+ (\Phi(\varphi_2, 1) \land \Phi(\varphi_1, 0)) \\
+\Phi(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, 1) &:=
+ (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land (\Phi(\varphi_1, 1) \lor \Phi(\varphi_3, 1)) \\
+\Phi(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, 0) &:=
+ (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor (\Phi(\varphi_1, 0) \land \Phi(\varphi_3, 0)) \\
+\Phi(\forall x_1, \dots, x_n. \varphi, 1) &:= \forall x_1, \dots, x_n. \Phi(\varphi, 1) \\
+\Phi(\exists x_1, \dots, x_n. \varphi, 1) &:= \exists x_1, \dots, x_n. \Phi(\varphi, 1) \\
+\Phi(\forall x_1, \dots, x_n. \varphi, 0) &:= \exists x_1, \dots, x_n. \Phi(\varphi, 0) \\
+\Phi(\exists x_1, \dots, x_n. \varphi, 0) &:= \forall x_1, \dots, x_n. \Phi(\varphi, 0) \\
+\Phi(\varphi, 1) &:= \varphi \\
+\Phi(\varphi, 0) &:= \neg\varphi
+\end{align*}
+
+\ruleparagraph{Remark.} This is a placeholder rule that combines the many steps
done during clausification.
+\end{RuleDescription}
-\end{proof-rule}
-
-\begin{proof-rule}{and}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.& \varphi_1 \land \dots \land \varphi_n&(\dots)\\
- \proofsep& j.& \varphi_k &(\currule\; i)\\
- \end{plList}
- \end{plContainer}
-and $1 \leq k \leq n$.
-\end{proof-rule}
-
-\begin{proof-rule}{not_or}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \lor \dots \lor \varphi_n) &(\dots)\\
-\proofsep& j.& \neg \varphi_k &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
+\begin{RuleDescription}{and}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1 \land \cdots \land \varphi_n$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_k$ & (\currule\;$i$) \\
+\end{AletheX}
and $1 \leq k \leq n$.
-\end{proof-rule}
-
-\begin{proof-rule}{or}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1 \lor \dots \lor \varphi_n &(\dots)\\
-\proofsep& j.& \varphi_1 , \dots , \varphi_n &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-
-\paragraph{Remark.} This rule deconstructs the \smtinline{or} operator
-into a clause denoted by $\smtinline{cl}$.
-
-\begin{rule-example}
-An application of the \currule{} rule.
+\end{RuleDescription}
-\begin{minted}{smtlib2.py -x}
+\begin{RuleDescription}{not_or}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n)$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg \varphi_k$ & (\currule\;$i$) \\
+\end{AletheX}
+and $1 \leq k \leq n$.
+\end{RuleDescription}
+
+\begin{RuleDescription}{or}
+\begin{AletheX}
+$i$. & \ctxsep &
+$\varphi_1 \lor \cdots \lor \varphi_n$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1, \dots, \varphi_n$ & (\currule\;$i$) \\
+\end{AletheX}
+
+\ruleparagraph{Remark.} This rule deconstructs the \inlineAlethe{or} operator
+into a clause denoted by \inlineAlethe{cl}.
+\end{RuleDescription}
+
+\begin{RuleExample}
+An application of the \proofRule{or} rule.
+\begin{AletheVerb}
(step t15 (cl (or (= a b) (not (<= a b)) (not (<= b a))))
:rule la_disequality)
(step t16 (cl (= a b) (not (<= a b)) (not (<= b a)))
:rule or :premises (t15))
-\end{minted}
-\end{rule-example}
-\end{proof-rule}
-
-\begin{proof-rule}{not_and}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \land \dots \land \varphi_n) &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \dots , \neg\varphi_n &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-
-\end{proof-rule}
-
-\begin{proof-rule}{xor1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \operatorname{xor} \varphi_1\;\varphi_2 &(\dots)\\
-\proofsep& j.& \varphi_1 , \varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{xor2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \operatorname{xor} \varphi_1\;\varphi_2 &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \neg\varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_xor1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg(\operatorname{xor} \varphi_1\;\varphi_2) &(\dots)\\
-\proofsep& j.& \varphi_1 , \neg\varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_xor2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg(\operatorname{xor} \varphi_1\;\varphi_2) &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{implies}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1\rightarrow\varphi_2 &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_implies1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1\rightarrow\varphi_2) &(\dots)\\
-\proofsep& j.& \varphi_1 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_implies2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1\rightarrow\varphi_2) &(\dots)\\
-\proofsep& j.& \neg\varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{equiv1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1\leftrightarrow\varphi_2 &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{equiv2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1\leftrightarrow\varphi_2 &(\dots)\\
-\proofsep& j.& \varphi_1 , \neg\varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_equiv1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg(\varphi_1\leftrightarrow\varphi_2) &(\dots)\\
-\proofsep& j.& \varphi_1 , \varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_equiv2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg(\varphi_1\leftrightarrow\varphi_2) &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \neg\varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{and_pos}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k &\currule\\
-\end{plList}
-\end{plContainer}
+\end{AletheVerb}
+\end{RuleExample}
+
+\begin{RuleDescription}{not_and}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 \land \dots \land \varphi_n)$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1 , \dots , \neg\varphi_n$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{xor1}
+\begin{AletheX}
+$i$. & \ctxsep & $\lsymb{xor}\,\varphi_1\,\varphi_2$
+ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1, \varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{xor2}
+\begin{AletheX}
+$i$. & \ctxsep & $\lsymb{xor}\,\varphi_1\,\varphi_2$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_xor1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg(\lsymb{xor}\,\varphi_1\,\varphi_2)$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_xor2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg(\lsymb{xor}\,\varphi_1\,\varphi_2)$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1 , \varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{implies}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1\rightarrow\varphi_2$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1, \varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_implies1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1\rightarrow\varphi_2)$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_implies2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1\rightarrow\varphi_2)$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{equiv1}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1≈\varphi_2$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1, \varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{equiv2}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1≈\varphi_2$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1, \neg\varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_equiv1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg(\varphi_1≈\varphi_2)$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1 , \varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_equiv2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg(\varphi_1≈\varphi_2)$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1, \neg\varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{and_pos}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$ & \currule \\
+\end{AletheX}
with $1 \leq k \leq n$.
-\end{proof-rule}
-
-\begin{proof-rule}{and_neg}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1
- , \dots , \neg\varphi_n &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{or_pos}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
- , \varphi_n &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{or_neg}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k &\currule\\
-\end{plList}
-\end{plContainer}
+\end{RuleDescription}
+
+\begin{RuleDescription}{and_neg}
+\begin{AletheX}
+$i$. & \ctxsep & $(\varphi_1 \land \cdots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{or_pos}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n) , \varphi_1 , \dots, \varphi_n$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{or_neg}
+\begin{AletheX}
+$i$. & \ctxsep & $(\varphi_1 \lor \cdots \lor \varphi_n), \neg \varphi_k$ & \currule \\
+\end{AletheX}
with $1 \leq k \leq n$.
-\end{proof-rule}
-
-\begin{proof-rule}{xor_pos1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \operatorname{xor} \varphi_2) , \varphi_1 , \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{xor_pos2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \operatorname{xor} \varphi_2)
-, \neg \varphi_1, \neg \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{xor_neg1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1 \operatorname{xor} \varphi_2
-, \varphi_1 , \neg \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{xor_neg2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1 \operatorname{xor} \varphi_2
-, \neg \varphi_1 , \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{implies_pos}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg (\varphi_1 \rightarrow \varphi_2)
-, \neg \varphi_1 , \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{implies_neg1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1 \rightarrow \varphi_2
-, \varphi_1 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{implies_neg2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \varphi_1 \rightarrow \varphi_2
-, \neg \varphi_2 &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{equiv_pos1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg (\varphi_1 \leftrightarrow \varphi_2) , \varphi_1 , \neg \varphi_2
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{equiv_pos2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\neg (\varphi_1 \leftrightarrow \varphi_2) , \neg \varphi_1 , \varphi_2
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{equiv_neg1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\varphi_1 \leftrightarrow \varphi_2 , \neg \varphi_1 , \neg \varphi_2
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{equiv_neg2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\varphi_1 \leftrightarrow \varphi_2 , \varphi_1 , \varphi_2
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{ite1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \operatorname{ite}\varphi_1\;\varphi_2\;\varphi_3 &(\dots)\\
-\proofsep& j.& \varphi_1 , \varphi_3 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{ite2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \operatorname{ite}\varphi_1\;\varphi_2\;\varphi_3 &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{ite_pos1}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.&
- \neg (\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3) , \varphi_1 , \varphi_3
- &\currule\\
- \end{plList}
- \end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{ite_pos2}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.&
- \neg (\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3) , \neg \varphi_1 , \varphi_2
- &\currule\\
- \end{plList}
- \end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{ite_neg1}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.&
- \operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3 , \varphi_1 , \neg \varphi_3
- &\currule\\
- \end{plList}
- \end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{ite_neg2}{veriT}
- \begin{plContainer}
- \begin{plList}
- \proofsep& i.&
- \operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3 , \neg \varphi_1 , \neg \varphi_2
- &\currule\\
- \end{plList}
- \end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_ite1}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg(\operatorname{ite}\varphi_1\;\varphi_2\;\varphi_3) &(\dots)\\
-\proofsep& j.& \varphi_1 , \neg\varphi_3 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{not_ite2}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \neg(\operatorname{ite}\varphi_1\;\varphi_2\;\varphi_3) &(\dots)\\
-\proofsep& j.& \neg\varphi_1 , \neg\varphi_2 &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{connective_def}{veriT}
+\end{RuleDescription}
+
+\begin{RuleDescription}{xor_pos1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1\,\lsymb{xor}\,\varphi_2) , \varphi_1 , \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{xor_pos2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1\,\lsymb{xor}\,\varphi_2), \neg \varphi_1, \neg \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{xor_neg1}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{xor_neg2}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1\,\lsymb{xor}\,\varphi_2, \neg \varphi_1, \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{implies_pos}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{implies_neg1}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1 \rightarrow \varphi_2, \varphi_1$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{implies_neg2}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1 \rightarrow \varphi_2, \neg \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{equiv_pos1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 ≈ \varphi_2), \varphi_1, \neg \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{equiv_pos2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\varphi_1 ≈ \varphi_2), \neg \varphi_1, \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{equiv_neg1}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1 ≈ \varphi_2, \neg \varphi_1, \neg \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{equiv_neg2}
+\begin{AletheX}
+$i$. & \ctxsep & $\varphi_1 ≈ \varphi_2, \varphi_1, \varphi_2$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite1}
+\begin{AletheX}
+$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1 , \varphi_3$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite2}
+\begin{AletheX}
+$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1, \varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite_pos1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3), \varphi_1, \varphi_3$ & (\currule) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite_pos2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg (\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3), \neg \varphi_1, \varphi_2$ & (\currule) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite_neg1}
+\begin{AletheX}
+$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, \varphi_1, \neg \varphi_3$ & (\currule) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite_neg2}
+\begin{AletheX}
+$i$. & \ctxsep & $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, \neg \varphi_1, \neg \varphi_2$ & (\currule) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_ite1}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3)$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1, \neg\varphi_3$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_ite2}
+\begin{AletheX}
+$i$. & \ctxsep & $\neg(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3)$ & ($\dots$) \\
+$j$. & \ctxsep & $\neg\varphi_1 , \neg\varphi_2$ & (\currule\;$i$) \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{connective_def}
This rule is used to replace connectives by their definition. It can be one
of the following:
-
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& \varphi_1\operatorname{xor}\varphi_2 \leftrightarrow
- (\neg\varphi_1 \land \varphi_2) \lor (\varphi_1 \land \neg\varphi_2)
- &\currule\\
- \end{plList}
- \end{plContainer}
-
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& \varphi_1\leftrightarrow\varphi_2 \leftrightarrow
- (\varphi_1 \rightarrow \varphi_2) \land (\varphi_2 \rightarrow \varphi_1)
- &\currule\\
- \end{plList}
- \end{plContainer}
-
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& \operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3 \leftrightarrow
- (\varphi_1 \rightarrow \varphi_2) \land (\neg\varphi_1 \rightarrow \varphi_3)
- &\currule\\
- \end{plList}
- \end{plContainer}
-
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& \forall x_1, \dots, x_n. \varphi \leftrightarrow \neg\exists x_1, \dots, x_n. \neg\varphi
- &\currule\\
- \end{plList}
- \end{plContainer}
-
-\end{proof-rule}
-
-\begin{proof-rule}{and_simplify}{veriT}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+ $\varphi_1\,\lsymb{xor}\,\varphi_2 ≈
+ (\neg\varphi_1 \land \varphi_2) \lor (\varphi_1 \land \neg\varphi_2)$ & \currule \\
+\end{AletheXS}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+ $\varphi_1≈\varphi_2 ≈
+ (\varphi_1 \rightarrow \varphi_2) \land (\varphi_2 \rightarrow \varphi_1)$ & \currule \\
+\end{AletheXS}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+ $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3 ≈
+ (\varphi_1 \rightarrow \varphi_2) \land (\neg\varphi_1 \rightarrow \varphi_3)$ & \currule \\
+\end{AletheXS}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+ $\forall x_1, \dots, x_n.\,\varphi ≈ \neg(\exists x_1, \dots, x_n.\,
+ \neg\varphi)$ & \currule \\
+\end{AletheXS}
+\end{RuleDescription}
+
+\begin{RuleDescription}{and_simplify}
This rule simplifies an $\land$ term by applying equivalent
transformations as long as possible. Hence, the general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \varphi_1\land \dots\land\varphi_n \leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\varphi_1\land \cdots\land\varphi_n ≈ \psi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\top \land \dots \land \top \leftrightarrow \top$
- \item $\varphi_1 \land \dots \land \varphi_n \leftrightarrow \varphi_1
- \land \dots \land \varphi_{n'} $ where the right hand side has all
+ \item $\top \land \cdots \land \top ⇒ \top$
+ \item $\varphi_1 \land \cdots \land \varphi_n ⇒ \varphi_1
+ \land \cdots \land \varphi_{n'} $ where the right-hand side has all
$\top$ literals removed.
- \item $\varphi_1 \land \dots \land \varphi_n \leftrightarrow \varphi_1
- \land \dots \land \varphi_{n'} $ where the right hand side has all
+ \item $\varphi_1 \land \cdots \land \varphi_n ⇒ \varphi_1
+ \land \cdots \land \varphi_{n'} $ where the right-hand side has all
repeated literals removed.
- \item $\varphi_1 \land\dots\land \bot\land\dots \land \varphi_n \leftrightarrow \bot$
- \item $\varphi_1 \land\dots\land \varphi_i\land \dots \land \varphi_j\land\dots \land \varphi_n \leftrightarrow \bot$
+ \item $\varphi_1 \land\cdots\land \bot\land\cdots \land \varphi_n ⇒ \bot$
+ \item $\varphi_1 \land\cdots\land \varphi_i\land \cdots \land \varphi_j\land\cdots \land \varphi_n ⇒ \bot$
and $\varphi_i$, $\varphi_j$ are such that
\begin{align*}
\varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
@@ -1034,32 +1017,28 @@ The possible transformations are:
\end{align*}
and one of $n, m$ is odd and the other even. Either can be $0$.
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{or_simplify}{veriT}
+\begin{RuleDescription}{or_simplify}
This rule simplifies an $\lor$ term by applying equivalent
transformations as long as possible. Hence, the general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& (\varphi_1\lor \dots\lor\varphi_n) \leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $(\varphi_1\lor \cdots\lor\varphi_n) ≈ \psi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\bot \lor \dots \lor \bot \leftrightarrow \bot$
- \item $\varphi_1 \lor \dots \lor \varphi_n \leftrightarrow \varphi_1
- \lor \dots \lor \varphi_{n'} $ where the right hand side has all
+ \item $\bot \lor \cdots \lor \bot ⇒ \bot$
+ \item $\varphi_1 \lor \cdots \lor \varphi_n ⇒ \varphi_1
+ \lor \cdots \lor \varphi_{n'} $ where the right-hand side has all
$\bot$ literals removed.
- \item $\varphi_1 \lor \dots \lor \varphi_n \leftrightarrow \varphi_1
- \lor \dots \lor \varphi_{n'} $ where the right hand side has all
+ \item $\varphi_1 \lor \cdots \lor \varphi_n ⇒ \varphi_1
+ \lor \cdots \lor \varphi_{n'} $ where the right-hand side has all
repeated literals removed.
- \item $\varphi_1 \lor\dots\lor \top\lor\dots \lor \varphi_n \leftrightarrow \top$
- \item $\varphi_1 \lor\dots\lor \varphi_i\lor \dots \lor \varphi_j\lor\dots \lor \varphi_n \leftrightarrow \top$
+ \item $\varphi_1 \lor\cdots\lor \top\lor\cdots \lor \varphi_n ⇒ \top$
+ \item $\varphi_1 \lor\cdots\lor \varphi_i\lor \cdots \lor \varphi_j\lor\cdots \lor \varphi_n ⇒ \top$
and $\varphi_i$, $\varphi_j$ are such that
\begin{align*}
\varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
@@ -1067,223 +1046,176 @@ The possible transformations are:
\end{align*}
and one of $n, m$ is odd and the other even. Either can be $0$.
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{not_simplify}{veriT}
+\begin{RuleDescription}{not_simplify}
This rule simplifies an $\neg$ term by applying equivalent
transformations as long as possible. Hence, the general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \neg\varphi \leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\neg\varphi ≈ \psi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\neg (\neg \varphi) \leftrightarrow \varphi$
- \item $\neg \bot \leftrightarrow \top$
- \item $\neg \top \leftrightarrow \bot$
+ \item $\neg (\neg \varphi) ⇒ \varphi$
+ \item $\neg \bot ⇒ \top$
+ \item $\neg \top ⇒ \bot$
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{implies_simplify}{veriT}
+\begin{RuleDescription}{implies_simplify}
This rule simplifies an $\rightarrow$ term by applying equivalent
transformations as long as possible. Hence, the general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \varphi_1\rightarrow \varphi_2 \leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\varphi_1\rightarrow \varphi_2 ≈ \psi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\neg \varphi_1 \rightarrow \neg \varphi_2 \leftrightarrow \varphi_2\rightarrow \varphi_1$
- \item $\bot \rightarrow \varphi \leftrightarrow \top$
- \item $ \varphi \rightarrow \top \leftrightarrow \top$
- \item $\top \rightarrow \varphi \leftrightarrow \varphi$
- \item $ \varphi \rightarrow \bot \leftrightarrow \neg \varphi$
- \item $ \varphi \rightarrow \varphi \leftrightarrow \top$
- \item $\neg \varphi \rightarrow \varphi \leftrightarrow \varphi$
- \item $ \varphi \rightarrow \neg \varphi \leftrightarrow \neg \varphi$
- \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 \leftrightarrow \varphi_1\lor \varphi_2$
+ \item $\neg \varphi_1 \rightarrow \neg \varphi_2 ⇒ \varphi_2\rightarrow \varphi_1$
+ \item $\bot \rightarrow \varphi ⇒ \top$
+ \item $ \varphi \rightarrow \top ⇒ \top$
+ \item $\top \rightarrow \varphi ⇒ \varphi$
+ \item $ \varphi \rightarrow \bot ⇒ \neg \varphi$
+ \item $ \varphi \rightarrow \varphi ⇒ \top$
+ \item $\neg \varphi \rightarrow \varphi ⇒ \varphi$
+ \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
+ \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒ \varphi_1\lor \varphi_2$
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{equiv_simplify}{veriT}
-This rule simplifies an $\leftrightarrow$ term by applying equivalent
+\begin{RuleDescription}{equiv_simplify}
+This rule simplifies a formula with the head symbol $≈\,: \lsymb{Bool}\,\lsymb{Bool}\,\lsymb{Bool}$
+by applying equivalent
transformations as long as possible. Hence, the general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& (\varphi_1\leftrightarrow \varphi_2) \leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $(\varphi_1≈ \varphi_2) ≈ \psi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $(\neg \varphi_1 \leftrightarrow \neg \varphi_2) \leftrightarrow ( \varphi_1\leftrightarrow \varphi_2)$
- \item $( \varphi\leftrightarrow \varphi) \leftrightarrow \top$
- \item $( \varphi\leftrightarrow \neg \varphi) \leftrightarrow \bot$
- \item $(\neg \varphi\leftrightarrow \varphi) \leftrightarrow \bot$
- \item $(\top \leftrightarrow \varphi) \leftrightarrow \varphi$
- \item $( \varphi \leftrightarrow \top) \leftrightarrow \varphi$
- \item $(\bot \leftrightarrow \varphi) \leftrightarrow \neg \varphi$
- \item $( \varphi \leftrightarrow \bot) \leftrightarrow \neg \varphi$
+ \item $(\neg \varphi_1 ≈ \neg \varphi_2) ⇒ ( \varphi_1≈ \varphi_2)$
+ \item $( \varphi≈ \varphi) ⇒ \top$
+ \item $( \varphi≈ \neg \varphi) ⇒ \bot$
+ \item $(\neg \varphi≈ \varphi) ⇒ \bot$
+ \item $(\top ≈ \varphi) ⇒ \varphi$
+ \item $( \varphi ≈ \top) ⇒ \varphi$
+ \item $(\bot ≈ \varphi) ⇒ \neg \varphi$
+ \item $( \varphi ≈ \bot) ⇒ \neg \varphi$
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{bool_simplify}{veriT}
+\begin{RuleDescription}{bool_simplify}
This rule simplifies a boolean term by applying equivalent
transformations as long as possible. Hence, the general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \varphi\leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\varphi≈ \psi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\neg(\varphi_1\rightarrow \varphi_2) \leftrightarrow (\varphi_1 \land \neg \varphi_2)$
- \item $\neg(\varphi_1\lor \varphi_2) \leftrightarrow (\neg \varphi_1 \land \neg \varphi_2)$
- \item $\neg(\varphi_1\land \varphi_2) \leftrightarrow (\neg \varphi_1 \lor \neg \varphi_2)$
- \item $(\varphi_1 \rightarrow (\varphi_2\rightarrow \varphi_3)) \leftrightarrow (\varphi_1\land \varphi_2) \rightarrow \varphi_3$
- \item $((\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2) \leftrightarrow (\varphi_1\lor \varphi_2)$
- \item $(\varphi_1 \land (\varphi_1\rightarrow \varphi_2)) \leftrightarrow (\varphi_1 \land \varphi_2)$
- \item $((\varphi_1\rightarrow \varphi_2) \land \varphi_1) \leftrightarrow (\varphi_1 \land \varphi_2)$
+ \item $\neg(\varphi_1\rightarrow \varphi_2) ⇒ (\varphi_1 \land \neg \varphi_2)$
+ \item $\neg(\varphi_1\lor \varphi_2) ⇒ (\neg \varphi_1 \land \neg \varphi_2)$
+ \item $\neg(\varphi_1\land \varphi_2) ⇒ (\neg \varphi_1 \lor \neg \varphi_2)$
+ \item $(\varphi_1 \rightarrow (\varphi_2\rightarrow \varphi_3)) ⇒ (\varphi_1\land \varphi_2) \rightarrow \varphi_3$
+ \item $((\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2) ⇒ (\varphi_1\lor \varphi_2)$
+ \item $(\varphi_1 \land (\varphi_1\rightarrow \varphi_2)) ⇒ (\varphi_1 \land \varphi_2)$
+ \item $((\varphi_1\rightarrow \varphi_2) \land \varphi_1) ⇒ (\varphi_1 \land \varphi_2)$
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
+\begin{RuleDescription}{ac_simp}
+ This rule simplifies nested occurrences of $\lor$ or $\land$:
-\begin{proof-rule}{ac_simp}{veriT}
- This rule simplifies nested occurences of $\lor$ or $\land$:
-
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& \psi \leftrightarrow \varphi_1 \circ\dots\circ\varphi_n
- &\currule\\
- \end{plList}
- \end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\psi ≈ \varphi_1 \circ\cdots\circ\varphi_n$ & \currule \\
+\end{AletheXS}
where $\circ \in \{\lor, \land\}$ and $\psi$ is a nested application of $\circ$.
The literals $\varphi_i$ are literals of the flattening of $\psi$ with duplicates
removed.
-\end{proof-rule}
-
-\subsubsection*{If-Then-Else Operators}
-\label{sec:ite-simp-rules}
+\end{RuleDescription}
-\begin{proof-rule}{ite_simplify}{veriT}
+\begin{RuleDescription}{ite_simplify}
This rule simplifies an if-then-else term by applying equivalent
- transformations until fix point\footnote{Note however that the order of the
+ transformations until fixed point\footnote{Note however that the order of the
application is important, since the set of rules is not confluent. For
- example, the term $(\operatorname{ite} \top \; t_1 \; t_2 \leftrightarrow
- t_1)$ can be simplified into both $p$ and $(not (not p))$ depending on the
+ example, the term $(\lsymb{ite} \top \; t_1 \; t_2 ≈
+ t_1)$ can be simplified into both $p$ and $(\neg (\neg p))$ depending on the
order of applications.}
%
-Depending on the sort of the
-$\operatorname{ite}$-term the rule can have one of two forms. If the sort
-is $\mathbf{Bool}$ it has the form
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \operatorname{ite} \varphi\;t_1\;t_2 \leftrightarrow \psi
-&\currule\\
-\end{plList}
-\end{plContainer}
-where $\psi$ is the transformed term.
+It has the form
-Otherwise, it has the form
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \operatorname{ite} \varphi\;t_1\;t_2 \simeq u
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\lsymb{ite}\,\varphi\,t_1\,t_2 ≈ u$ & \currule \\
+\end{AletheXS}
where $u$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\operatorname{ite} \top \; t_1 \; t_2 \leftrightarrow t_1$
- \item $\operatorname{ite} \bot \; t_1 \; t_2 \leftrightarrow t_2$
- \item $\operatorname{ite} \psi \; t \; t \leftrightarrow t$
- \item $\operatorname{ite} \neg \varphi \; t_1 \; t_2 \leftrightarrow \operatorname{ite} \varphi \; t_2 \; t_1$
- \item $\operatorname{ite} \psi \; (\operatorname{ite} \psi\;t_1\;t_2)\; t_3 \leftrightarrow
- \operatorname{ite} \psi\; t_1\; t_3$
- \item $\operatorname{ite} \psi \; t_1\; (\operatorname{ite} \psi\;t_2\;t_3) \leftrightarrow
- \operatorname{ite} \psi\; t_1\; t_3$
- \item $\operatorname{ite} \psi \; \top\; \bot \leftrightarrow \psi$
- \item $\operatorname{ite} \psi \; \bot\; \top \leftrightarrow \neg\psi$
- \item $\operatorname{ite} \psi \; \top \; \varphi \leftrightarrow \psi\lor\varphi$
- \item $\operatorname{ite} \psi \; \varphi\;\bot \leftrightarrow \psi\land\varphi$
- \item $\operatorname{ite} \psi \; \bot\; \varphi \leftrightarrow \neg\psi\land\varphi$
- \item $\operatorname{ite} \psi \; \varphi\;\top \leftrightarrow \neg\psi\lor\varphi$
+ \item $\lsymb{ite}\, \top \, t_1 \, t_2 ⇒ t_1$
+ \item $\lsymb{ite}\, \bot \, t_1 \, t_2 ⇒ t_2$
+ \item $\lsymb{ite}\, \psi \, t \, t ⇒ t$
+ \item $\lsymb{ite}\, \neg \varphi \, t_1 \, t_2 ⇒ \lsymb{ite}\, \varphi \, t_2 \, t_1$
+ \item $\lsymb{ite}\, \psi \, (\lsymb{ite}\, \psi\,t_1\,t_2)\, t_3 ⇒
+ \lsymb{ite}\, \psi\, t_1\, t_3$
+ \item $\lsymb{ite}\, \psi \, t_1\, (\lsymb{ite}\, \psi\,t_2\,t_3) ⇒
+ \lsymb{ite}\, \psi\, t_1\, t_3$
+ \item $\lsymb{ite}\, \psi \, \top\, \bot ⇒ \psi$
+ \item $\lsymb{ite}\, \psi \, \bot\, \top ⇒ \neg\psi$
+ \item $\lsymb{ite}\, \psi \, \top \, \varphi ⇒ \psi\lor\varphi$
+ \item $\lsymb{ite}\, \psi \, \varphi\,\bot ⇒ \psi\land\varphi$
+ \item $\lsymb{ite}\, \psi \, \bot\, \varphi ⇒ \neg\psi\land\varphi$
+ \item $\lsymb{ite}\, \psi \, \varphi\,\top ⇒ \neg\psi\lor\varphi$
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{qnt_simplify}{veriT}
+\begin{RuleDescription}{qnt_simplify}
This rule simplifies a $\forall$-formula with a constant predicate.
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& \forall x_1, \dots, x_n. \varphi \leftrightarrow \varphi
- &\currule\\
- \end{plList}
- \end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\forall x_1, \dots, x_n. \varphi ≈ \varphi$ & \currule \\
+\end{AletheXS}
where $\varphi$ is either $\top$ or $\bot$.
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{onepoint}{veriT}
+\begin{RuleDescription}{onepoint}
The {\currule} rule is the ``one-point-rule''. That is: it eliminates quantified
variables that can only have one value.
-\begin{plContainer}
-\begin{plContainer}
-\begin{plSubList}
-\plLine\\
-\Gamma, x_{k_1},\dots, x_{k_m}, x_{j_1} \mapsto t_{j_1}, \dots , x_{j_o} \mapsto t_{j_o},
-\proofsep& j.& \varphi \leftrightarrow \varphi' &(\dots)\\
-\end{plSubList}
-\begin{plList}
-\Gamma \proofsep& k.&
-Q x_1, \dots, x_n.\varphi \leftrightarrow Q x_{k_1}, \dots, x_{k_m}. \varphi' &\currule\\
-\end{plList}
-\end{plContainer}
-\end{plContainer}
+\begin{AletheXS}
+\aletheLineS
+$j$. & \spctx{$\Gamma, x_{k_1},\dots, x_{k_m}, x_{j_1} \mapsto t_{j_1}, \dots , x_{j_o} \mapsto t_{j_o}$}
+ & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
+ \spsep
+$k$. & & \ctxsep & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
+\end{AletheXS}
where $Q\in\{\forall, \exists\}$, $n = m + o$, $k_1, \dots, k_m$ and
$j_1, \dots, j_o$ are monotone
mappings to $1, \dots, n$, and no $x_{k_i}$ appears in $x_{j_1}, \dots, x_{j_o}$.
The terms $t_{j_1}, \dots, t_{j_o}$ are the points of the variables
-$x_{j_1}, \dots, x_{j_o}$. Points are defined by equalities $x_i\simeq t_i$
+$x_{j_1}, \dots, x_{j_o}$. Points are defined by equalities $x_i≈ t_i$
with positive polarity in the term $\varphi$.
-\paragraph{Remark.} Since an eliminated variable $x_i$ might appear free in a
+\ruleparagraph{Remark.} Since an eliminated variable $x_i$ might appear free in a
term $t_j$, it is necessary to replace $x_i$ with $t_i$ inside $t_j$. While
this substitution is performed correctly, the proof for it is currently
missing.
+\end{RuleDescription}
-\begin{rule-example}
-An application of the $\currule$ rule on the term $\forall x, y.\, x \simeq y
-\rightarrow f(x)\land f(y)$ look like this:
+\begin{RuleExample}
+An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x ≈ y
+\rightarrow (f\,x)\land (f\,y))$ look like this:
-\begin{minted}{smtlib2.py -x}
+\begin{AletheVerb}
(anchor :step t3 :args ((:= y x)))
(step t3.t1 (cl (= x y)) :rule refl)
(step t3.t2 (cl (= (= x y) (= x x)))
@@ -1293,410 +1225,310 @@ An application of the $\currule$ rule on the term $\forall x, y.\, x \simeq y
:rule cong :premises (t3.t3))
(step t3.t5 (cl (= (and (f x) (f y)) (and (f x) (f x))))
:rule cong :premises (t3.t4))
-(step t3.t6 (cl (=
- (=> (= x y) (and (f x) (f y)))
- (=> (= x x) (and (f x) (f x)))))
+(step t3.t6 (cl (= (=> (= x y) (and (f x) (f y)))
+ (=> (= x x) (and (f x) (f x)))))
:rule cong :premises (t3.t2 t3.t5))
(step t3 (cl (=
(forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
- (forall ((x S)) (=> (= x x) (and (f x) (f x))))))
+ (forall ((x S)) (=> (= x x) (and (f x) (f x))))))
:rule qnt_simplify)
-\end{minted}
-\end{rule-example}
-
-\end{proof-rule}
-
-\begin{proof-rule}{qnt_join}{veriT}
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep& i.&
- Q x_1, \dots, x_n. Q x_{n+1}, \dots, x_{m}. \varphi
- \leftrightarrow
- Q x_{k_1}, \dots, x_{k_o}. \varphi
- &\currule\\
- \end{plList}
- \end{plContainer}
+\end{AletheVerb}
+\end{RuleExample}
+
+\begin{RuleDescription}{qnt_join}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $Q x_1, \dots, x_n.\,(Q x_{n+1}, \dots, x_{m}.\,\varphi)
+ ≈ Q x_{k_1}, \dots, x_{k_o}.\,\varphi$ & \currule \\
+\end{AletheXS}
where $m > n$ and $Q\in\{\forall, \exists\}$. Furthermore, $k_1, \dots, k_o$ is a monotonic
map to $1, \dots, m$ such that $x_{k_1}, \dots, x_{k_o}$ are pairwise
distinct, and $\{x_1, \dots, x_m\} = \{x_{k_1}, \dots, x_{k_o}\}$.
-\end{proof-rule}
-
-\begin{proof-rule}{qnt_rm_unused}{veriT}
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep& i.&
- Q x_1, \dots, x_n. \varphi \leftrightarrow Q x_{k_1}, \dots, x_{k_m}.\varphi
- &\currule\\
- \end{plList}
- \end{plContainer}
+\end{RuleDescription}
+
+\begin{RuleDescription}{qnt_rm_unused}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $Q x_1, \dots, x_n.\,\varphi ≈ Q x_{k_1}, \dots, x_{k_m}.\,\varphi$
+ & \currule \\
+\end{AletheXS}
where $m \leq n$ and $Q\in\{\forall, \exists\}$. Furthermore, $k_1, \dots, k_m$ is
a monotonic map to $1, \dots, n$ and if $x\in \{x_j\; |\; j \in \{1, \dots,
- n\} \land j\not\in \{k_1, \dots, k_m\}\}$ then $x$ is not free in $P$.
+ n\} \land j\in\not \{k_1, \dots, k_m\}\}$ then $x$ is not free in $P$.
+\end{RuleDescription}
-\end{proof-rule}
-
-\begin{proof-rule}{eq_simplify}{veriT}
- This rule simplifies an $\simeq$ term by applying equivalent
+\begin{RuleDescription}{eq_simplify}
+ This rule simplifies an $≈$ term by applying equivalent
transformations as long as possible. Hence, the general form is
- \begin{plContainer}
- \begin{plList}
- \Gamma\proofsep&
- i.& t_1\simeq t_2 \leftrightarrow \varphi
- &\currule\\
- \end{plList}
- \end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $(t_1≈ t_2) ≈ \varphi$ & \currule \\
+\end{AletheXS}
where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $t \simeq t \leftrightarrow \top$
- \item $t_1 \simeq t_2 \leftrightarrow \bot$ if $t_1$ and $t_2$ are different numeric constants.
- \item $\neg (t \simeq t) \leftrightarrow \bot$ if $t$ is a numeric constant.
+ \item $t ≈ t ⇒ \top$
+ \item $(t_1 ≈ t_2) ⇒ \bot$ if $t_1$ and $t_2$ are different numeric constants.
+ \item $\neg (t ≈ t) ⇒ \bot$ if $t$ is a numeric constant.
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{div_simplify}{veriT}
+\begin{RuleDescription}{div_simplify}
This rule simplifies a division by applying equivalent
transformations. The general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& (t_1 / t_2) \simeq t_3
-&\currule\\
-\end{plList}
-\end{plContainer}
-
-\noindent The possible transformations are:
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $(t_1\, /\, t_2) ⇒ t_3$ & \currule \\
+\end{AletheXS}
+The possible transformations are:
\begin{itemize}
- \item $t/t = 1$
- \item $t/1 = t$
- \item $t_1 / t_2 = t_3$
- if $t_1$ and $t_2$ are constants and $t_3$ is $t_1$
- divided by $t_2$ according to the semantic of the current theory.
+ \item $t\, /\, t ⇒ 1$
+ \item $t\, /\, 1 ⇒ t$
+ \item $t_1\, /\, t_2 ⇒ t_3$
+ if $t_1$ and $t_2$ are constants and $t_3$ is $t_1$
+ divided by $t_2$ according to the semantic of the current theory.
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{prod_simplify}{veriT}
+\begin{RuleDescription}{prod_simplify}
This rule simplifies a product by applying equivalent
transformations as long as possible. The general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& t_1\times\dots\times t_n \simeq u
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $t_1\times\cdots\times t_n ≈ u$ & \currule \\
+\end{AletheXS}
where $u$ is either a constant or a product.
The possible transformations are:
\begin{itemize}
- \item $t_1\times\dots\times t_n = u$ where all
+ \item $t_1\times\cdots\times t_n ⇒ u$ where all
$t_i$ are constants and $u$ is their product.
- \item $t_1\times\dots\times t_n = 0$ if any
+ \item $t_1\times\cdots\times t_n ⇒ 0$ if any
$t_i$ is $0$.
- \item $t_1\times\dots\times t_n =
- c \times t_{k_1}\times\dots\times t_{k_n}$ where $c$
- ist the product of the constants of $t_1, \dots, t_n$ and
- $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
- with the constants removed.
- \item $t_1\times\dots\times t_n =
- t_{k_1}\times\dots\times t_{k_n}$: same as above if $c$ is
- $1$.
+ \item $t_1\times\cdots\times t_n ⇒
+ c \times t_{k_1}\times\cdots\times t_{k_n}$ where $c$
+ is the product of the constants of $t_1, \dots, t_n$ and
+ $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
+ with the constants removed.
+ \item $t_1\times\cdots\times t_n ⇒
+ t_{k_1}\times\cdots\times t_{k_n}$: same as above if $c$ is $1$.
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{unary_minus_simplify}{veriT}
+\begin{RuleDescription}{unary_minus_simplify}
This rule is either
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& - (-t) \simeq t &\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $- (-t) ≈ t$ & \currule \\
+\end{AletheXS}
or
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& -t \simeq u &\currule\\
-\end{plList}
-\end{plContainer}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $-t ≈ u$ & \currule \\
+\end{AletheXS}
where $u$ is the negated numerical constant $t$.
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{minus_simplify}{veriT}
+\begin{RuleDescription}{minus_simplify}
This rule simplifies a subtraction by applying equivalent
transformations. The general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& t_1 - t_2 \simeq u &\currule\\
-\end{plList}
-\end{plContainer}
-
-\noindent The possible transformations are:
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $t_1- t_2 ≈ u$ & \currule \\
+\end{AletheXS}
+The possible transformations are:
\begin{itemize}
- \item $t - t = 0$
- \item $t_1 - t_2 = t_3$ where $t_1$
+ \item $t - t ⇒ 0$
+ \item $t_1 - t_2 ⇒ t_3$ where $t_1$
and $t_2$ are numerical constants and $t_3$ is $t_2$ subtracted
from~$t_1$.
- \item $t - 0 = t$
- \item $0 - t = -t$
+ \item $t - 0 ⇒ t$
+ \item $0 - t ⇒ -t$
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{sum_simplify}{veriT}
+\begin{RuleDescription}{sum_simplify}
This rule simplifies a sum by applying equivalent
transformations as long as possible. The general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& t_1+\dots+t_n \simeq u &\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $t_1+\cdots+t_n ≈ u$ & \currule \\
+\end{AletheXS}
where $u$ is either a constant or a product.
The possible transformations are:
\begin{itemize}
- \item $t_1+\dots+t_n = c$ where all
+ \item $t_1+\cdots+t_n ⇒ c$ where all
$t_i$ are constants and $c$ is their sum.
- \item $t_1+\dots+t_n =
- c + t_{k_1}+\dots+t_{k_n}$ where $c$
- ist the sum of the constants of $t_1, \dots, t_n$ and
- $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
- with the constants removed.
- \item $t_1+\dots+t_n =
- t_{k_1}+\dots+t_{k_n}$: same as above if $c$ is
- $0$.
+ \item $t_1+\cdots+t_n ⇒
+ c + t_{k_1}+\cdots+t_{k_n}$ where $c$
+ is the sum of the constants of $t_1, \dots, t_n$ and
+ $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
+ with the constants removed.
+ \item $t_1+\cdots+t_n ⇒
+ t_{k_1}+\cdots+t_{k_n}$: same as above if $c$ is
+ $0$.
\end{itemize}
-\end{proof-rule}
+\end{RuleDescription}
-\begin{proof-rule}{comp_simplify}{veriT}
+\begin{RuleDescription}{comp_simplify}
This rule simplifies a comparison by applying equivalent
transformations as long as possible. The general form is
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& t_1 \bowtie t_n \leftrightarrow \psi &\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $t_1 \bowtie t_n ≈ \psi$ & \currule \\
+\end{AletheXS}
where $\bowtie$ is as for the proof rule \proofRule{la_generic}, but never
-$\simeq$.
+$≈$.
The possible transformations are:
\begin{itemize}
- \item $t_1 < t_2 \leftrightarrow \varphi$ where $t_1$ and
+ \item $t_1 < t_2 ⇒ \varphi$ where $t_1$ and
$t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
strictly greater than $t_2$ and $\bot$ otherwise.
- \item $t < t \leftrightarrow \bot$
- \item $t_1 \leq t_2 \leftrightarrow \varphi$ where $t_1$ and
+ \item $t < t ⇒ \bot$
+ \item $t_1 \leq t_2 ⇒ \varphi$ where $t_1$ and
$t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
greater than $t_2$ or equal and $\bot$ otherwise.
- \item $t \leq t \leftrightarrow \top$
- \item $t_1 \geq t_2 \leftrightarrow t_2 \leq t_1$
- \item $t_1 < t_2 \leftrightarrow \neg (t_2 \leq t_1)$
- \item $t_1 > t_2 \leftrightarrow \neg (t_1 \leq t_2)$
+ \item $t \leq t ⇒ \top$
+ \item $t_1 \geq t_2 ⇒ t_2 \leq t_1$
+ \item $t_1 < t_2 ⇒ \neg (t_2 \leq t_1)$
+ \item $t_1 > t_2 ⇒ \neg (t_1 \leq t_2)$
\end{itemize}
-\end{proof-rule}
-
-\begin{proof-rule}{let}{veriT}
- This rule eliminats $\operatorname{let}$. It has the form
-
- \begin{plContainer}
- \begin{plList}
- \Gamma \proofsep& i_1.& t_{1} \simeq s_{1} &(\dots)\\
- \plLine\\
- \Gamma \proofsep& i_n.& t_{n} \simeq s_{n} &(\dots)\\
- \end{plList}
- \begin{plSubList}
- \plLine\\
- \Gamma, x_1 \mapsto s_1, \dots, x_n \mapsto s_n,
- \proofsep& j.& u\simeq u' &(\dots)\\
- \end{plSubList}
- \begin{plList}
- \Gamma \proofsep& k.&
- (\operatorname{let} x_1 := t_1, \dots, x_n := t_n. u) \simeq
- u'
- &(\currule\;i_1 \dots i_n)\\
- \end{plList}
- \end{plContainer}
- where $\simeq$ is replaced by $\leftrightarrow$ where necessary.
-
- The premise $i_1, \dots, i_n$ must be in the same subproof as
- the $currule$ step. If for $t_i\simeq s_i$ the $t_i$ and $s_i$
- are syntactically equal, the premise
+\end{RuleDescription}
+
+\begin{RuleDescription}{let}
+ This rule eliminates $\lsymb{let}$. It has the form
+
+\begin{AletheXS}
+$i_1$. & $\Gamma$ & \ctxsep & $t_{1} ≈ s_{1}$ & ($\dots$) \\
+\aletheLineS
+$i_n$. & $\Gamma$ & \ctxsep & $t_{n} ≈ s_{n}$ & ($\dots$) \\
+\aletheLineS
+$j$. & \spctx{$\Gamma, x_1 \mapsto s_1, \dots, x_n \mapsto s_n$}
+ & \ctxsep & $u ≈ u'$ & ($\dots$) \\
+\spsep
+$k$. & $\Gamma$ & \ctxsep &
+ $(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u) ≈ u'$
+ & (\currule{}\;$i_1$, \dots, $i_n$) \\
+\end{AletheXS}
+
+ The premise $i_1, \dots, i_n$ must be in the same subproof as
+ the \currule{} step. If for $t_i≈ s_i$ the $t_i$ and $s_i$
+ are syntactically equal, the premise
is skipped.
+\end{RuleDescription}
-\end{proof-rule}
-
-\begin{proof-rule}{distinct_elim}{veriT}
-This rule eliminates the $\operatorname{distinct}$ predicate. If called with one
+\begin{RuleDescription}{distinct_elim}
+This rule eliminates the $\lsymb{distinct}$ predicate. If called with one
argument this predicate always holds:
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-(\operatorname{distinct} t) \leftrightarrow \top
-&\currule\\
-\end{plList}
-\end{plContainer}
-
-If applied to terms of type $\mathbf{Bool}$ more than two terms can never be
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $(\lsymb{distinct}\, t) ≈ \top$ & \currule \\
+\end{AletheXS}
+
+If applied to terms of type $\lsymb{Bool}$ more than two terms can never be
distinct, hence only two cases are possible:
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-(\operatorname{distinct} \varphi\;\psi) \leftrightarrow \neg (\varphi \leftrightarrow \psi)
-&\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+$(\lsymb{distinct}\,\varphi\,\psi) ≈ \neg (\varphi ≈ \psi)$ & \currule \\
+\end{AletheXS}
and
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-(\operatorname{distinct} \varphi_1\;\varphi_2\;\varphi_3\dots) \leftrightarrow \bot
-&\currule\\
-\end{plList}
-\end{plContainer}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+$(\lsymb{distinct}\,\varphi_1\,\varphi_2\,\varphi_3\,\dots) ≈ \bot$ & \currule \\
+\end{AletheXS}
The general case is
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-(\operatorname{distinct} t_1 \dots t_n) \leftrightarrow
-\bigwedge_{i=1}^{n}\bigwedge_{j=i+1}^{n} t_i\;{\not\simeq}\;t_j
-&\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{la_rw_eq}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-(t \simeq u) \simeq (t \leq u \land u \leq t)
-&\currule\\
-\end{plList}
-\end{plContainer}
-
-\paragraph{Remark.} While the connective could be $\leftrightarrow$,
-currently an equality is used.
-\end{proof-rule}
-
-\begin{proof-rule}{nary_elim}{veriT}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ &
+$(\lsymb{distinct}\,t_1\,\dots\, t_n) ≈
+\bigwedge_{i=1}^{n}\bigwedge_{j=i+1}^{n} t_i\;{\not≈}\;t_j$ & \currule \\
+\end{AletheXS}
+\end{RuleDescription}
+
+\begin{RuleDescription}{la_rw_eq}
+\begin{AletheX}
+$i$. & \ctxsep & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ & \currule \\
+\end{AletheX}
+\end{RuleDescription}
+
+\begin{RuleDescription}{nary_elim}
This rule replaces $n$-ary operators with their equivalent
application of the binary operator. It is never applied to $\land$ or $\lor$.
-Thre cases are possible.
+Three cases are possible.
If the operator $\circ$ is left associative, then the rule has the form
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \bigcirc_{i=1}^{n} t_i \leftrightarrow
-(\dots( t_1\circ t_2) \circ t_3)\circ \dots t_n) &\currule\\
-\end{plList}
-\end{plContainer}
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\bigcirc_{i=1}^{n} t_i ≈ (\dots( t_1\circ t_2) \circ t_3)\circ \cdots t_n)$
+ & \currule \\
+\end{AletheXS}
If the operator $\circ$ is right associative, then the rule has the form
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \bigcirc_{i=1}^{n} t_i \leftrightarrow
-( t_1 \circ \dots \circ ( t_{n-2} \circ ( t_{n-1} \circ t_n)\dots) &\currule\\
-\end{plList}
-\end{plContainer}
-
-If the operator is \emph{chainable}, then it has the form
-\begin{plContainer}
-\begin{plList}
-\Gamma\proofsep&
-i.& \bigcirc_{i=1}^{n} t_i \leftrightarrow
-( t_1\circ t_2) \land ( t_2 \circ t_3) \land \dots
-\land ( t_{n-1}\circ t_n) &\currule\\
-\end{plList}
-\end{plContainer}
-\end{proof-rule}
-
-\begin{proof-rule}{bfun_elim}{veriT}
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& \psi &(\dots)\\
-\proofsep& j.& \varphi &(\currule\; i)\\
-\end{plList}
-\end{plContainer}
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\bigcirc_{i=1}^{n} t_i ≈
+( t_1 \circ \cdots \circ ( t_{n-2} \circ ( t_{n-1} \circ t_n)\dots)$ & \currule \\
+\end{AletheXS}
+
+If the operator is {\em chainable}, then it has the form
+
+\begin{AletheXS}
+$i$. & \ctxsep & $\Gamma$ & $\bigcirc_{i=1}^{n} t_i ≈
+( t_1\circ t_2) \land ( t_2 \circ t_3) \land \cdots
+\land ( t_{n-1}\circ t_n)$ & \currule \\
+\end{AletheXS}
+\end{RuleDescription}
+
+\begin{RuleDescription}{bfun_elim}
+\begin{AletheX}
+$i$. & \ctxsep & $\psi$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi$ & (\currule\; $i$) \\
+\end{AletheX}
The formula $\varphi$ is $\psi$ after boolean functions have been simplified.
This happens in a two step process. Both steps recursively iterate over $\psi$.
-The first step expands quantified variable of type $\mathbf{Bool}$. Hence,
-$\exists x.t$ becomes $t[x\mapsto \bot]\lor t[x\mapsto \top]$ and
-$\forall x.t$ becomes $t[x\mapsto \bot]\land t[x\mapsto \top]$. If $n$ variables of sort
-$\mathbf{Bool}$ appear in a quantifier, the disjunction (conjunction) has
+The first step expands quantified variable of type $\lsymb{Bool}$. Hence,
+$(\exists x.\,t)$ becomes $t[x\mapsto \bot]\lor t[x\mapsto \top]$ and
+$(\forall x.\,t)$ becomes $t[x\mapsto \bot]\land t[x\mapsto \top]$. If $n$ variables of sort
+$\lsymb{Bool}$ appear in a quantifier, the disjunction (conjunction) has
$2^n$ terms. Each term replaces the variables in $t$ according
to the bits of a number which is increased by one for each subsequent
term starting from zero. The left-most variable corresponds to the
least significant bit.
The second step expands function argument of boolean types by introducing
-appropriate if-then-else terms. For example, consider $f(x, P, y)$ where
-$P$ is some formula. Then we replace this term by $\operatorname{ite} P\;
-f(x, \top, y)\;f(x, \bot, y)$. If the argument is already the constant $\top$
+appropriate if-then-else terms. For example, consider $(f\,x\, P\, y)$ where
+$P$ is some formula. Then we replace this term by $(\lsymb{ite}\, P\,
+(f\,x\, \top\ y)\,(f\,x\, \bot\, y))$. If the argument is already the constant $\top$
or $\bot$, it is ignored.
-
-\end{proof-rule}
-
-\begin{proof-rule}{ite_intro}{veriT}
-Either
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.& t \simeq (t' \land u_1 \land \dots \land u_n) &\currule\\
-\end{plList}
-\end{plContainer}
-or
-\begin{plContainer}
-\begin{plList}
-\proofsep& i.&
-\varphi \leftrightarrow (\varphi' \land u_1 \land \dots \land u_n) &\currule\\
-\end{plList}
-\end{plContainer}
-
-The term $t$ (the formula $\varphi$) contains the $\operatorname{ite}$ operator.
-Let $s_1, \dots, s_n$ be the terms starting with $\operatorname{ite}$, i.e.
-$s_i := \operatorname{ite} \psi_i\;r_i\;r'_i$, then $u_i$ has the form
-\begin{equation*}
- \operatorname{ite} \psi_i\;(s_i \simeq r_i)\;(s_i \simeq r'_i)
-\end{equation*}
-or
-\begin{equation*}
- \operatorname{ite} \psi_i\;(s_i \leftrightarrow r_i)\;(s_i \leftrightarrow r'_i)
-\end{equation*}
-if $s_i$ is of sort $\mathbf{Bool}$. The term $t'$ (the formular
-$\varphi'$) is equal to the term $t$ (the formular $\varphi'$) up to the
-reordering of equalities where one argument is an $\operatorname{ite}$
+\end{RuleDescription}
+
+\begin{RuleDescription}{ite_intro}
+\begin{AletheX}
+$i$. & \ctxsep & $t ≈ (t' \land u_1 \land \dots \land u_n)$ & (\currule) \\
+\end{AletheX}
+
+The term $t$ (the formula $\varphi$) contains the $\lsymb{ite}$ operator.
+Let $s_1, \dots, s_n$ be the terms starting with $\lsymb{ite}$, i.e.
+$s_i := \lsymb{ite}\,\psi_i\,r_i\,r'_i$, then $u_i$ has the form
+\[
+ \lsymb{ite}\,\psi_i\,(s_i ≈ r_i)\,(s_i ≈ r'_i)
+\]
+The term $t'$ is equal to the term $t$ up to the
+reordering of equalities where one argument is an $\lsymb{ite}$
term.
-\paragraph{Remark.} This rule stems from the introduction of fresh
+\ruleparagraph{Remark.} This rule stems from the introduction of fresh
constants for if-then-else terms inside veriT. Internally $s_i$ is a new
constant symbol and the $\varphi$ on the right side of the equality is
$\varphi$ with the if-then-else terms replaced by the constants. Those
constants are unfolded during proof printing. Hence, the slightly strange
form and the reordering of equalities.
-\end{proof-rule}
-
-% \subsection*{Experimental Proof Rules}
-% \label{sec:exp-rules}
-
-% \begin{proof-rule}{deep_skolemize}{veriT}
-% This rule is only emitted when the option \texttt{--enable-deep-skolem}
-% is given. This option is experimental and should not be used.
-% \end{proof-rule}
+\end{RuleDescription}
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "doc"
-%%% End:
+\clearpage
+\subsection{Index of Rules}
+\printindex[rules]
diff --git a/spec/spec.tex b/spec/spec.tex
index aeb5c6e4ab6b1ee403bd9ac8976065a101d155d9..ad3093489d1c4bcc6f949ed836f99d1acda29248 100644
--- a/spec/spec.tex
+++ b/spec/spec.tex
@@ -1647,7 +1647,7 @@ is functional congruence, and \proofRule{sko_forall} works like
\section{The Alethe Rules}
\label{apx:rules}
-\input{alethe_rules}
+\input{rule_list}
\clearpage
\section*{Changelog}