Remove overloading of \bar{}

It was used in a few places to represent complementary literals,
but is mostly used to represent vectors of terms, variables.  This
commit removes the usage for complementary literals.  The few
places that used it now define the complement manually.

spec/doc.tex

@@ -442,24 +442,9 @@ terms of sort $\mathbf{Bool}$.
 %
 We use $=$ to denote syntactic equality and $\simeq$ to denote the sorted
 equality predicate.
-%
-We also use the notion of complementary literals
-very liberally: $\varphi = \bar{\psi}$ holds if the terms obtained
-after removing all leading negations from $\varphi$ and $\bar{\psi}$
-are syntactically equal and the number of leading negations is even
-for $\varphi$ and odd for $\psi$, or vice versa.  To simplify the
+To simplify the
 notation we will omit the sort of terms when possible.
-\begin{comment}{Haniel Barbosa}
-  This notation is clashing with the notation of sequences of symbols, like in
-  $\bar x$ for $x_1, \dots, x_n$.
-
-  Maybe we could use an alternative notation for ``normalization under double
-  negation elimination''? Like $\llfloor \varphi \rrfloor_{\neg\neg}$? I find
-  the use of ``complementary literal'' to refer this a bit confusing
-  anyway. There are very few uses in the rules (only tautology, and/or simps),
-  so we could even not introduce a notation and just refer to ``normalized under
-  double negation elimination''.
-\end{comment}
+
 \begin{example} The following example shows a simple Alethe proof.
 It uses quantifier instantiation and resolution to show a contradiction.
 The sections below step-by-step describe the concepts necessary to

spec/rule_list.tex

@@ -87,7 +87,12 @@ serves only informational purpose.
       \proofsep& j.& \top &(\currule; i)\\
     \end{plList}
   \end{plContainer}
-  and $\varphi_i = \bar\varphi_j$.
+  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{proof-rule}
 
 \begin{proof-rule}{contraction}{veriT}
@@ -986,8 +991,13 @@ The possible transformations are:
     \land \dots \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$ if
-      $\varphi_i = \bar{\varphi_j}$
+    \item $\varphi_1 \land\dots\land \varphi_i\land \dots \land \varphi_j\land\dots \land \varphi_n \leftrightarrow \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{proof-rule}
 
@@ -1014,8 +1024,13 @@ The possible transformations are:
     \lor \dots \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$ if
-    	$\varphi_i = \bar{\varphi_j}$
+    \item $\varphi_1 \lor\dots\lor \varphi_i\lor \dots \lor \varphi_j\lor\dots \lor \varphi_n \leftrightarrow \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{proof-rule}