 (\exists \overline{x}. \varphi_2)\big) \leftrightarrow \exists \overline{x}. (\varphi_1 \vee \varphi_2)$\\
  \hline
  
  \multicolumn{3}{|c|}{\bf Term algebra specific proof rules}\\ 
  \hline
  $\textsc{$\exists$-{Subst}}\xspace$ && $\exists z. t \land (z = u) \leftrightarrow t[u/z], \textrm{if~}z \not\in\mathit{var}(u)$\\
  
  $\textsc{$\exists$-{Gen}}\xspace$ && $z=(f\, \overline{t}) \leftrightarrow \exists \overline{y}. z=(f\, \overline{y}) \wedge \overline{y} = \overline{t}$, $\textrm{if~}\overline{y} \not\in \mathit{var}\big((f\, \overline{t})\big) \cup \{z\}$ \\ 
  \hline
  \end{tabular}
  \caption{The macro rules used to generate proof objects for antiunification. The $\odot$ is a placeholder for one logical operator in the set $\{\land, \leftrightarrow\}$. Also, unless explicitly delimited using parentheses, the scope of the quantifiers extends as much as possible to the right.}
  \label{fig:macro-rules}
 
  \end{figure}
  


\subsection{Proof object schema $\vee_\mathit{gen}$\xspace}
\label{sec:orgen}

The first step of our method is to establish the equivalence between the disjunction $t_1 \vee t_2$  and the encoding of the initial unification problem $\langle z, z \mapsto t_1 \sqcup t_2\rangle$, that is  $\big(\exists z. z \land (z = t_1)\big) \vee  \big(\exists z.   z \land (z = t_2)\big)$. 
This is done via the proof object schema $\vee_\mathit{gen}$\xspace, which is shown below.

To shorten our presentation, the \textsc{ModusPonens} rule from Figure~\ref{fig:proofsystem} is applied here directly over a double implication $\leftrightarrow$ (instead of $\rightarrow$).
For the steps k$\mathop{+}$6 and k$\mathop{+}$8 we use \textsc{Propositional} to justify two trivial equivalences: the first says that $\phi_1 \vee \phi_2 \leftrightarrow \phi_1' \vee \phi_2'$ if $\phi_1 \leftrightarrow \phi_1'$ and $\phi_2 \leftrightarrow \phi_2'$; the second is just a well-known distributivity property.\\
\begin{center}
\begin{tabular}{|l|l|l|}
\hline
(k) &$\big(\exists z. t_1 \leftrightarrow  z \land (z = t_1)\big)$ & \textsc{$\exists$-{Subst}}\xspace (note: $z[t_1/z] = t_1$) \\
\hline
(k$\mathop{+}$1) &$\big(\exists z. t_1 \leftrightarrow  z \land (z = t_1)\big) \leftrightarrow \big(t_1 \leftrightarrow \exists z. z \land (z = t_1)\big) $ & \textsc{$\exists$-Scope}\xspace \\
\hline
(k$\mathop{+}$2) & $t_1 \leftrightarrow \exists z. z \land (z = t_1)$ & \textsc{ModusPonens}: k, k+1\\
\hline
(k$\mathop{+}$3) &$\big(\exists z. t_2 \leftrightarrow  z \land (z = t_2)\big)$ & \textsc{$\exists$-{Subst}}\xspace (note: $z[t_2/z] = t_2$) \\
\hline
(k$\mathop{+}$4) &$\big(\exists z. t_2 \leftrightarrow  z \land (z = t_2)\big) \leftrightarrow \big(t_2 \leftrightarrow \exists z. z \land (z = t_2)\big)$ & \textsc{$\exists$-Scope}\xspace \\
\hline
(k$\mathop{+}$5) & $t_2 \leftrightarrow \exists z. z \land (z = t_2)$ & \textsc{ModusPonens}: k+3, k+4\\
\hline

(k$\mathop{+}$6) & $t_1 \vee t_2 \leftrightarrow \big(\exists z. z \land (z = t_1)\big) \vee  \big(\exists z.   z \land (z = t_2)\big)$ & \textsc{Propositional}: k+2, k+5\\
\hline

(k$\mathop{+}$7) & $\Big(\big(\exists z.  z \land (z = t_1)\big) \vee  \big(\exists z. z \land (z = t_2)\big) \Big)\leftrightarrow$ &\\
&  \hfill$\exists z. \big(z \land (z = t_1)\big) \vee  \big(  z \land (z = t_2)\big)$ & \textsc{$\exists$-Collapse}\xspace \\
\hline

(k$\mathop{+}$8) & $\big( z \land (z = t_1)\big) \vee  \big(z \land (z = t_2)\big) \leftrightarrow $ &  \\
& $ z \land \big((z = t_1) \vee  (z = t_2)\big)$ & \textsc{Propositional} \\
\hline

(k$\mathop{+}$9) & $\exists z. \big( z \land (z = t_1)\big) \vee  \big(z \land (z = t_2)\big) \leftrightarrow$ &  \\
& $ \exists z. z \land \big((z = t_1) \vee  (z = t_2)\big)$ & \textsc{$\exists$-Ctx}\xspace: k$\mathop{+}$8 \\
\hline

(k$\mathop{+}$10) & $t_1 \vee t_2 \leftrightarrow \exists z. \big(z \land (z = t_1)\big) \vee  \big(  z \land (z = t_2)\big)$ & $\leftrightarrow_{\mathit{tranz}}$: k$\mathop{+}$6, k$\mathop{+}$7 \\
\hline

(k$\mathop{+}$11) & $t_1 \vee t_2 \leftrightarrow \exists z. z \land \big((z = t_1) \vee  (z = t_2)\big)$ & $\leftrightarrow_{\mathit{tranz}}$: k$\mathop{+}$10, k$\mathop{+}$9\\

\hline
\end{tabular}
\end{center}


\aaa{Am mai adaugat niste propozitii la fiecare dintre sectiunile care urmeaza: pentru e-gen', dec si step. }

\subsection{Proof schema $\rightsquigarrow_\mathit{step}$\xspace}
\label{sec:decaunif}

The proof schema of $\rightsquigarrow_\mathit{step}$\xspace used two other (sub)schemata \textsc{$\exists$-{Gen}}\xspace' and \textsc{Dec}\xspace. We explain these first, and them we present the proof schema for $\rightsquigarrow_\mathit{step}$\xspace.

\subsubsection{Proof object schema \textsc{$\exists$-{Gen}}\xspace'}
\label{sec:existsgenprim}

Recall that $\textsc{$\exists$-{Gen}}\xspace$ (Figure~\ref{fig:macro-rules} -- term algebra specific rule) establishes an equivalence between
$z=(f\, \overline{t})$ and $\exists \overline{y}. z=(f\, \overline{y}) \wedge \overline{y} = \overline{t}$, $\textrm{if~}\overline{y} \not\in \mathit{var}\big((f\, \overline{t})\big) \cup \{z\}$, which basically describes a generalisation of $(f\, \overline{t})$. 
However, most of the times $\textsc{$\exists$-{Gen}}\xspace$ is applied under a conjunction.
The proof schema $\textsc{$\exists$-{Gen}}\xspace'$ generalises the $\textsc{$\exists$-{Gen}}\xspace$ macro rule as follows:\\[1ex]
\centerline{$\big(\varphi \land z = (f\,\overline{t})\big) \leftrightarrow \exists \overline{z}. \varphi \land z = (f\,\overline{z}) \land \overline{z} = \overline{t},$}\\[1ex]
\noindent
where $(f\,\overline{t})$ denotes $(f\,t_1\,\ldots\,t_n)$, $ (f\,\overline{z})$ stands for  $(f\,z_1\,\ldots\,z_n