\documentclass[a4paper,11pt]{llncs}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{color}
\usepackage{array}
\usepackage{url}
%\usepackage{hyperref,breakurl}
\usepackage{versions}\excludeversion{ignore}
%\usepackage{amssymb,amsthm,latexsym,amsmath,mathdots}
\usepackage{amssymb,latexsym,amsmath,mathdots}
\usepackage{epstopdf}
\usepackage[dvipsnames,svgnames]{pstricks}

\pagestyle{plain}


%%% Jeremy's commands
\newcommand{\frwd}[2]{#1 `` #2}

%%% Raj's commands

\newcommand{\ltr}[3]{#2 <_{\tiny #1} #3}
\newcommand{\gtr}[3]{#2 >_{\tiny #1} #3}
\newcommand{\comp}[2]{#1 \;\mathtt{o}\; #2}
\newcommand{\trun}[3]{\{#1 \!\mid\! #2 \!\mid\! #3\}}
\newcommand{\biun}[2]{\{#1 \!\mid\! #2\}}
%\newcommand{\biun}[2]{(#1 \cup #2)}
\newcommand{\trans}[1]{#1^{\ast}}

%%% Nachum's commands
\newcommand{\cA}{DodgerBlue}
\newcommand{\cB}{Black}
\newcommand{\cC}{Crimson}
\newcommand{\A}{{\color{\cA}A}}
\newcommand{\B}{{\color{\cB}B}}
\newcommand{\C}{{\color{\cC}C}}
%\newtheorem{theorem}{Theorem}
%\newtheorem{corollary}{Corollary}
\let\rel=\mathrel
\newcommand{\stack}[1]{{\def\\{|}{\{#1\}}}}
\newcommand{\rstack}[1]{\rel{\stack{#1}}}


\title{Well-founded Unions Verified}
\author{
Jeremy Dawson\inst{1}
\and
Nachum Dershowitz\inst{2}
\and
Rajeev Gor\'e\inst{1}
}

\institute{
Research School of Computer Science, Australian National University
\and
School of Computer Science, Tel Aviv University 
}


\begin{document}
\sloppy
\maketitle
\begin{abstract}
  Given $n > 1$ well-founded binary relations $R_1, R_2, \cdots ,
  R_n$, when is their union $\bigcup_{i=1}^{n} R_i$ also
  well-founded~? We first describe two sets of incomparable conditions
  and the pen-and-paper proofs for $n=3$ due to Dershowitz. We then
  describe conditions and machine-checked proofs for $n=4$ due to
  Dawson and Gor\'e. We finally describe general conditions and
  machine-checked proofs for arbitrary $n$ due to Dawson and Gor\'e.
\end{abstract}

\section{Introduction}

A binary relation $R$ over some underlying set is well-founded if
there is no infinite \textit{ascending} chain
$ x_0 \; R \; x_1 \; R \; \cdots \; R \; x_{n-1} \; R \; x_{n} \; R \;
\cdots $
Thus, by \emph{well-founded}, we mean the absence of infinite
forward-pointing paths.  Lescanne~\cite{lescanne-rewriting-list} as
well as
Blass and Gurevich~\cite{blass-gurevich-termination} give some of the
history of well-foundedness based on Ramsey's
Theorem~\ref{thm:ramsey} (below).

%
Given $n \geq 3$ well-founded binary relations
$R_1, R_2, \cdots , R_n$ over some common underlying set,
when is their union
$\bigcup_{i=1}^{n} R_i$ also well-founded~? 

To garner insight, we first tackle just three relations, $A$, $B$, and $C$
and refer to the relations as ``colours''. We then extend our
results to $n=4$ and finally describe the general pattern for
arbitrary $n$. All proofs have been machine-checked using Isabelle/HOL
and are available at
\url{www.cecs.anu.edu.au:~jeremy/}

\section{Well-founded Tri-partite Unions}
\label{sec:well-founded-tri}

Assuming that $A,B$ and $C$ are all well-founded binary relations over
some set of elements, let us use the following shorthand notations:
\begin{center}
\begin{tabular}{l@{\extracolsep{1cm}}cl}
$\biun{A}{B}$ & stands for & $A \cup B$
\\
$AB$ & stands for &
$\{(x,z) \mid \exists y. (x,y) \in A \;\&\; (y,z) \in B\}$
\\
$\trans{C}$ & stands for &
the transitive closure of $C$
\end{tabular}
\end{center}
\marginpar{reflexive and
  transitive closure ? YES}


\begin{theorem}[Ramsey]\label{thm:ramsey}
  The union
  $\trun{A}{B}{C}$
  is well-founded if
  \begin{equation}
    \label{eq:1}
      \trun{A}{B}{C}\trun{A}{B}{C} \subseteq \trun{A}{B}{C}
  \end{equation}
\end{theorem}

% \begin{theorem}[Ramsey]
% The union $\stack{A\\B\\C}$ is well-founded if
% \begin{eqnarray}
% \stack{A\\B\\C} \stack{A\\B\\C} & \subseteq & \stack{A\\B\\C}
% \end{eqnarray}
% \end{theorem}

\begin{proof}
  The infinite version of Ramsey's Theorem applies when the union is
  transitive, so that every two (distinct) nodes within an infinite
  chain in the union of the colours has a coloured (directed) edge.
  Then, there must lie an infinite monochrome subchain within any
  infinite chain, contradicting the well-foundedness of each colour
  alone.%
% \footnote{See
% Alfons Geser, \textit{Relative Termination}, Ph.D.\@ dissertation, Fakult\"at fu\"r Mathematik und Informatik, Universit\"at Passau, Germany, 1990 (Report 91-03, Ulmer Informatik-Berichte, Universit\"at Ulm, 1991; available at \url{http://homepage.cs.uiowa.edu/~astump/papers/geser_ dissertation.pdf}).}
\qed
\end{proof}

Only three of the nine cases are actually needed for the limited
outcome that we are seeking, an infinite monochromic path, rather than
a clique as in Ramsey's Theorem, as we observe next.

\begin{theorem}[Dershowitz]\label{thm:dersh2}
The union $\stack{A\\B\\C}$ is well-founded if
\begin{eqnarray}
%B A \cup CA \cup CB & \subseteq & \stack{A\\B\\C} \;.
\trun{BA}{CA}{CB} & \subseteq & \stack{A\\B\\C} \;.
\end{eqnarray}
\end{theorem}

\begin{proof}
  When the union is not well-founded, there is an infinite path
  $X=\{x_i\}_i$ with each edge from $x_i$ to $X_{i+1}$ one of $A$,
  $B$, or $C$.  Extract a maximal subsequence $\{x_{i_j}\}_j$ of $X$
  such that $x_{i_j} \rel{A} x_{i_{j+1}}$ for each $j$.  If it's
  finite, then repeat at the first opportunity in the tail.  If any is
  infinite, we have our contradiction.  If they're all finite, then
  consider the first occurrence of $x \rstack{B\\C} y \rel{A} z$.
  Since we could not take an $A$-step from $x$, or we would have, the
  conditions tell us that $x \rstack{B\\C} z$.  Swallowing up all such
  (non-initial) $A$-steps in this way, we are left with an infinite
  chain in $B\cup C$, for which we also know that no $A$-steps are
  possible anywhere.  Now extract maximal $B$-chains and then erase
  them, replacing $x \rel{C} y \rel{B} z$ with $x \rel{C} z$ ($A$- and
  $B$-steps having been precluded), leaving an infinite chain coloured
  purely $C$.
\qed
\end{proof}

\begin{corollary}[Dershowitz]
If $A$, $B$, and $C$ are transitive and
\begin{eqnarray*}
B A \cup CA \cup CB & \subseteq & \stack{A\\B\\C} \;,
\end{eqnarray*}
then, whenever there is an infinite path in the union $\stack{A\\B\\C}$, there is an infinite monochromatic clique.
\end{corollary}

Let's call the existence of an infinite ascending
chain in the union $\stack{A\\B\\C}$-\emph{immortality}.
%
We can do considerably better than the previous theorem:

\begin{theorem}[Tripartite]\label{thm:tripartite}
The union $\stack{A\\B\\C}$ is well-founded if
\begin{eqnarray}
\stack{B\\C} A  & \subseteq & A\stack{A\\B\\C}^* \cup B \cup C\\\nonumber
CB  & \subseteq & A\stack{A\\B\\C}^* \cup BB^* \cup C \;.
\end{eqnarray}
\end{theorem}

\begin{proof}
  We first construct an infinite chain $X=\{x_i\}_i$, in which an
  $A$-step is always preferred over $B$ or $C$, as long as immortality
  is maintained.  To do this, we start with an immortal element
  $x_0\in V$.  At each stage in the construction, if the chain so far
  ends in $x_i$, we look to see if there is any $y$ such that
  $x_i \rel{A} y$ and from which proceeds some infinite chain in the
  union, in which case $y$ is chosen to be $x_{i+1}$.  Otherwise,
  $x_{i+1}$ is any immortal element $z$ such that $x_i \rel{B} z$ or
  $x_i \rel{C} z$.

  If there are infinitely many $B$'s and/or $C$'s in $X$, use
  them---by means of the first condition---to remove all subsequent
  $A$-steps, leaving only $B$- and $C$-steps going out of points from
  which $A$ leads of necessity to mortality.  From what remains, if
  there is any $C$-step at a point where one could take one or more
  $B$-steps to anyplace later in the chain, take the latter route
  instead.  What remains now are $C$-steps at points where $BB^*$
  detours are also precluded.  If there are infinitely many such
  $C$-steps, then applying the condition for $CB$ will result in a
  pure $C$-chain, because neither $A\stack{A\\B\\C}^* $ nor $ BB^*$
  are options.  \qed
\end{proof}

Dropping $C$ from the conditions of the previous theorem, one gets the
criterion of Doornbos and Burghard von Karger~\cite{dvk} for
well-foundedness of the union of two well-founded relations $A$ and
$B$, called ``jumping'' by Dershowitz~\cite{dershowitz-jumping} and
called \verb!dvk_cond! in the sequel:
\begin{description}
\item[\rm jumping:] \qquad\qquad $B A  \subseteq  A\stack{A\\B}^* \cup B \;.$
\end{description}

Applying this criterion twice, one gets somewhat different
(incomparable) conditions for well-foundedness.
 
\begin{theorem}[Jumping I]
The union $\stack{A\\B\\C}$ is well-founded if
\begin{eqnarray*}
B A & \subseteq & A\stack{A\\B}^* \cup B\\%\nonumber
C \stack{A\\B} & \subseteq & \stack{A\\B}\stack{A\\B\\C}^* \cup C \;.
\end{eqnarray*}
\end{theorem}

\begin{proof}
The first inequality is the jumping criterion.
The second is the same with $C$ for $B$ and $\stack{A\\B}$ in place of $A$.
\qed
\end{proof}

For two relations, jumping provides a substantially weaker criterion for well-foundedness than does the appeal to Ramsey.
But for three,
whereas jumping allows more than one step for $BA$ (in essence, $A A^* B^*$),
it doesn't allow for $C$, which Ramsey does.

Switching r\^oles, start with jumping for $\stack{B\\C}$ before
combining with $A$, we get slightly different conditions yet:
\begin{theorem}[Jumping II]
The union $\stack{A\\B\\C}$ is well-founded if
\begin{eqnarray*}
CB & \subseteq & B\stack{B\\C}^* \cup C \\\nonumber
\stack{B\\C}A & \subseteq & A\stack{A\\B\\C}^* \cup B \cup C\;.
\end{eqnarray*}
\end{theorem}

Both this version of jumping and our tripartite condition allow
\begin{eqnarray*}
\stack{B\\C}A & \subseteq & A\stack{A\\B\\C}^* \cup B \cup C\\
CB & \subseteq & BB^* \cup C \;.
\end{eqnarray*}
They differ in that jumping also allows
the condition shown below on the left 
whereas tripartite has the one shown on the right instead:
\begin{center}
\begin{tabular}{l@{\extracolsep{3cm}}l}
jumping allows & tripartite allows\\[1em]
$CB \subseteq  B\stack{B\\C}^*$
& $CB \subseteq A\stack{A\\B\\C}^*$
\end{tabular}
\end{center}


Sadly, we cannot have the best of both worlds.
Let's color edges $\A$, $\B$, and $\C$ with
(solid) {\color{DodgerBlue}azure}, (dotted) black, and (dashed) {\color{Crimson}crimson} ink, respectively.
The graph below
only has multicolored loops
despite satisfying
\begin{equation*}
\begin{array}{rcl}
\stack{\B\\\C}\A & \subseteq & \C\\
\C \B & \subseteq & \A \cup \B\stack{\B\\\C}^* \;.
\end{array}
\end{equation*}

\begin{center}
\begin{pspicture}(-4,-1.5)(4,2)
\psline[linewidth=1.5pt,linecolor=Crimson,linestyle=dashed,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=1.5pt,linecolor=Black,linestyle=dotted]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=1.5pt,linecolor=DodgerBlue,,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=1.5pt,linecolor=Black,linestyle=dotted,linearc=2]{->}(3.9,0.1)(3,1.5)(-2,1.5)(-3.9,0.1) % z->v
\psline[linewidth=1.5pt,linecolor=Crimson,linestyle=dashed,linearc=2]{->}(-0.9,0.1)(1.4,0.9) % x->y
\psline[linewidth=1.5pt,linecolor=Black,linestyle=dotted,linearc=2]{->}(1.6,0.9)(3.9,0) % y->z
\rput(-4,0){$\bullet$}\rput(-1,0){$\bullet$}\rput(1.5,1){$\bullet$}\rput(4,0){$\bullet$} % vxyz
\end{pspicture}
\end{center}

Even
\begin{equation*}
\begin{array}{rcl}
\stack{\B\\\C}\A & \subseteq & \C\\
\C \B & \subseteq & \B\stack{\A\\\B}^*
\end{array}
\end{equation*}
doesn't work. To wit, the double loop in 
the graph below
harbours no monochrome subchain:
\begin{center}
\begin{pspicture}(-4,-1.5)(4,2)
\psline[linewidth=1.5pt,linecolor=Crimson,linestyle=dashed,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=1.5pt,linecolor=Black,linestyle=dotted]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=1.5pt,linecolor=DodgerBlue,,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=1.5pt,linecolor=Black,linestyle=dotted,linearc=2]{->}(3.9,0.1)(3,1.5)(-2,1.5)(-3.9,0.1) % z->v
\rput(-4,0){$\bullet$}\rput(-1,0){$\bullet$}\rput(4,0){$\bullet$} % vxz
\end{pspicture}
\end{center}

By the same token, the putative hypothesis below left is countered by the
graph below right:

\begin{center}
\begin{tabular}{lr}
  \begin{math}
\begin{array}{rcl}
\B \A  \cup \C \B & \subseteq & \C\\
\C \A & \subseteq & \B \A^* 
\end{array}
  \end{math}
&
\begin{pspicture}(-5,-1.5)(4,2)
\psline[linewidth=1.5pt,linecolor=Crimson,linestyle=dashed,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=1.5pt,linecolor=Black,linestyle=dotted]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=1.5pt,linecolor=DodgerBlue,,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=1.5pt,linecolor=DodgerBlue,linearc=2]{->}(3.9,0.1)(3,1.5)(-2,1.5)(-3.9,0.1) % z->v
\rput(-4,0){$\bullet$}\rput(-1,0){$\bullet$}\rput(4,0){$\bullet$} % vxz
\end{pspicture}
\end{tabular}
\end{center}

\section{Verifying these theorems in Isabelle}

In Section~\ref{sec:well-founded-tri},
we 
%Dershowitz~\cite{d-tri-un}
started with 
Theorems~\ref{thm:ramsey} and~\ref{thm:dersh2}, and proved
Theorem~\ref{thm:tripartite}, which is a
considerable improvement of 
Theorems~\ref{thm:ramsey} and~\ref{thm:dersh2}.
Now, we start with Theorem~\ref{thm:tripartite}, which we call
\texttt{wfp\_tri}.
\marginpar{Why is there no prime here but there is one later on?
It's not wf\_tri and wf\_tri'.  And I have changed D to BC.  
wf\_tri has the definition of BC and of dvk\_cond expanded.
I'll put current versions of both following statement of theorem.}
In the sequel, we write each definition and theorem in both plain text
and in Isabelle notation to highlight the correspondeces.


\begin{definition}\label{def:wf}
In Isabelle, the well-foundedness and composition of relations
is defined as follows where 
$x <_R y$ 
means 
$(x, y) \in R$:
\begin{enumerate}
\item A relation $R$ is well-founded if there is no infinite
%  decreasing sequence
descending chain
%$$\ldots <_R x_n <_R x_{n-1} <_R \ldots <_R x_1 <_R x_0$$
$$
  \ltr{R}{\ldots}{}
  \ltr{R}{x_n}{}
  \ltr{R}{x_{n-1}}{}
  \ltr{R}{\ldots}{}
  \ltr{R}{x_1}{x_0}
$$
\begin{verbatim}
wf ?r == ALL P. 
           (ALL x. (ALL y. (y, x) : ?r --> P y) --> P x) 
         --> (ALL x. P x)
\end{verbatim}
\item The composition $\comp{R}{S}$ of relations $R$ and $S$ is defined by
%$$R \circ S = \{(x, z). \exists y. (x, y) \in S \& (y, z) \in R\}$$
$$ \comp{R}{S} = \{(x, z) \mid \exists y. (x, y) \in S \;\&\; (y, z) \in R\}$$
\end{enumerate}

%  rel_comp_def:
\begin{verbatim}
   ?r O ?s == {(x, z). EX y. (x, y) : ?s & (y, z) : ?r}
\end{verbatim}
  
\end{definition}

In Definition~\ref{def:wf}, the question mark symbol \texttt{?}
indicates implicit universal quantification and so \texttt{?r} and
\texttt{?s} are free variables (parameters) that are instantiated.

Since \emph{both} $\comp{}{}$ and the definition \texttt{wf} of
well-founded used in Isabelle are the opposite of those used in
Section~\ref{sec:well-founded-tri}, the theorems in the sequel capture
the same notions.  If only one were different, we would have to
reverse the order of relation composition to make the two notions coincide.

\begin{definition}[\texttt{dvk\_cond} $\equiv$ jumping]\label{def:dvk-cond}
Following Doornbos and von Karger~\cite{dvk}, we define
a binary condition
${dvk\_cond}\; D \; A$
as:
$$D \circ A \subseteq (A \circ (A \cup D)^*) \cup D$$
%$$\comp{D}{A} \subseteq (A \circ (\trans{\biun{A}{D}}) \cup D$$
% dvk_cond_def':        
\begin{verbatim}
 dvk_cond ?d ?a == ?d O ?a <= (?a O (?a Un ?d)^*) Un ?d
 FOLLOWING is dvk_cond_def
 val it = "dvk_cond ?s ?r == ?s O ?r <= dvk_rel ?s ?r" : Thm.thm
\end{verbatim}
% \begin{verbatim}
%  dvk_cond_def':        
%     "dvk_cond ?s ?r == ?s O ?r <= (?r O (?r Un ?s)^*) Un ?s"
% \end{verbatim}
\marginpar{why the prime in \texttt{dvk\_cond\_def'}?
Without the prime, it is in terms of dvk\_rel, above}
\end{definition}

In Definition~\ref{def:dvk-cond},
\texttt{O} is Isabelle's relational composition operator from
Definition~\ref{def:wf}; 
\texttt{Un} is Isabelle's set-union operator; and
\texttt{<=} is $\subseteq$.
%
%We next restate Dershowitz's Theorem~3~\cite[Thm~3]{d-tri-un} where
%$\texttt{O}$ is Isabelle's composition operator;
%\verb!^*! is transitive closure.
%$\texttt{Un}$ is set-union;
%$\texttt{<=}$ is $\subseteq$; and
%\verb!?! indicates variables which are implicitly universally quantified:

% BEGIN: TO BE MOVED OR DELETED TO BE MOVED OR DELETED

% \renewcommand\theenumi{\alph{enumi}}
% \renewcommand\labelenumi{(\theenumi)}

% \begin{theorem}[\texttt{wf\_tri'}, Dershowitz, Theorem~3]
% \label{d-th3}
% Given three binary relations $A,B$ and $C$,
% their tripartite union $A \cup B \cup C$ is well-founded if
% all of the following hold:
% \begin{quote}
% \begin{enumerate}
% \item\label{wff-ABC} each of $A, B, C$ are well-founded;
% \item\label{disbunc} $D = (B \cup C)$;
% \item\label{dvk-A-BC} $dvk\_cond ~D~ A$ ;
% % $D \circ A \subseteq (A \circ (A \cup D)^*) \cup D$;
% % \item\label{dvk-A-BC} $(B \cup C) \circ A \subseteq 
% %   (A \circ (A \cup B \cup C)^*) \cup (B \cup C)$ where
% \item\label{d-th3-2} $C \circ B \subseteq 
%   (A \circ (A \cup D)^*) \cup (B \circ B^*) \cup C$.
% \end{enumerate}
% \end{quote}
% \begin{verbatim}
% wf_tri':  "[| 
%     wf ?A ; wf ?B ; wf ?C ; 
%     ?D = ?B Un ?C ; 
%     dvk_cond ?D ?A ;
%     ?C O ?B <= (?A O (?A Un ?D)^*) Un (?B O ?B^*) Un ?C
%     |] ==> wf (?A Un ?D)"
% \end{verbatim}
% \end{theorem}

% END: TO BE MOVED OR DELETED

We separate Dershowitz's proof of the Tripartite
Theorem~\ref{thm:tripartite} into a number of lemmas.  Note how,
generally, statements in the proof of the form ``there exists an
infinite chain'' have to be translated into a (contra-positive) lemma
with hypotheses and conclusion that certain relations are
well-founded, or that something is in the well-founded part of a
relation.

\begin{definition}[wfp R]
The well-founded part
of a relation $R$, written \texttt{wfp R}, is the set whose elements 
are not the head of any infinite descending $R$-chain.
\begin{verbatim}
val wfpI = 
   "ALL y. (y, ?x) : ?r --> y : wfp ?r ==> ?x : wfp ?r"
\end{verbatim}
\end{definition}

The only elements which can be shown to be in \texttt{wfp r} by
repeated applications of this rule are in \texttt{wfp r}. So a
relation $R$ over an underlying set $V$ is well-founded if and only
if\marginpar{JED, is this correct? YES}
every member of the underlying set $V$ is in the well-founded part of $R$.
The complement operation is written as \verb!-! in Isabelle, thus
\verb!- wfp R!  is the set of those elements which are the head of an
infinite descending $R$-chain.

% Following Dershowitz, we say an \emph{$R$-immortal} element is the head of
% an infinite descending $R$-chain,
% %in $R$,
% and ``\emph{immortal}'' means $(A \cup D)$-immortal, or
% $(A \cup B \cup C)$-immortal, as the case may be.


% \begin{lemma}[\texttt{wfp\_tri\_lem\_BC}] \label{lem-BC}
% If $B$ and $C$ are well-founded, 
% and condition (\ref{d-th3-2}) of Theorem~\ref{d-th3} is satisfied, 
% then in any infinite descending $B \cup C$-chain 
% there must be $C$-step(s) of the form $(y, z)$ where
% $z$ is the head of an infinite descending $A \cup B \cup C$-chain
% which starts with an $A$-step.
% \begin{verbatim}
% wfp_tri_lem_BC:
%    "[| ?D = ?B Un ?C; ?C O ?B <= (?A O (?A Un ?D)^*) Un (?B O ?B^*) Un ?C;
%          wf ?B; wf ?C |]
%       ==> ?x : wfp (?B Un ?C Int {(y, z). z ~: ?A `` (- wfp (?A Un ?D))})"
% \end{verbatim}
% \end{lemma}

% \begin{proof}
% Assume that $B$ and $C$ are well-founded.
% Define $C^-$ to be $C$, but excluding steps of the form $(w, z)$
% where there exists some $y$ such that $(y, z) \in A$ and
% $y$ is $A \cup B \cup C$-immortal.

% Suppose, contrary to the lemma, that $B \cup C^-$ is not well-founded.
% So there exists an $B \cup C^-$-immortal $z$.
% Choose $z$ to be $B$-minimal such,
% and also to be $C$-minimal among possible $B$-minimal choices.

% As $z$ is $B$-minimal, the first step
% of an infinite $B \cup C^-$-chain must be (say) $(y, z) \in C^-$.
% As $B$ is well-founded,
% let $y$ be $B$-minimal among possible choices for $y$.
% Then, by the $C$-minimality of $z$, although $y$ is $B \cup C^-$-immortal,
% it is not $B$-minimal among $B \cup C^-$-immortal members.
% So we have $(x, y) \in B$, where $x$ is $B \cup C^-$-immortal. 
% So as $C \circ B \subseteq (A \circ (A \cup B \cup C)^*) \cup
%   (B \circ B^*) \cup C$, 
% we could replace $z >_C >_B x$ in the infinite chain by 
% \begin{itemize}
% \item $(x, z) \in A \circ (A \cup B \cup C)^*$,
% say $(x, y') \in (A \cup B \cup C)^*$ and $(y', z) \in A$ ---
% but $x$ is $B \cup C^-$-immortal,
% and so is the head of an infinite descending
% $A \cup B \cup C$-chain, contradicting that $(y, z) \in C^-$,
% \item $(x, z) \in B \circ B^*$, 
%   which would contradict our choice of $z$ to be $B$-minimal
% \item $(x, z) \in C$ (and so $(x, z) \in C^-$) 
%   which would contradict our choice of $y$ to be $B$-minimal,
%   since $x$ could have been chosen instead of $y$.
% \end{itemize}
% Thus, in each case we get a contradiction, so $B \cup C^-$ is well-founded.
% \qed
% \end{proof}

% \begin{proof}
% By Lemma~\ref{lem-dvk} it is enough to prove that $D^-$ is well-founded.
% By Lemma~\ref{lem-BC} we have that $B \cup C^-$ is well-founded,
% and clearly $D^- \subseteq B \cup C^-$.
% \qed
% \end{proof}

% \section{Proving Results from the paper 
%   Nachum Dershowitz: Tripartite Unions}


% \begin{proof}
% Consider an infinite descending $A \cup R$-chain.  
% As $A$ is well-founded, from any point in this chain there must be another
% $R$-step.
% Wherever possible replace a $R$-step $z >_R v$ 
% followed by an $A$-step $v >_A u$
% by an $A$-step (possibly followed by a number of $A$- or $R$-steps)
% in the given chain.
% (This relates to the part 
% $R \circ A \subseteq (A \circ (A \cup R)^*) \cup \ldots$
% of \texttt{dvk\_cond}).
% Alternatively, if possible, replace the remainder of the chain from this
% point by any other infinite chain $z >_A y >_{A \cup R} \ldots$.
% Again, this will not always be possible since $A$ is well-founded.

% So, where this is not possible, we can
% replace a $R$-step followed by an $A$-step by a single $R$-step,
% which is possible using the part 
% $R \circ A \subseteq \ldots \cup R$ of \texttt{dvk\_cond}.

% Doing this repeatedly could absorb any number of $A$-steps, but, again,
% as $A$ is well-founded there cannot be infinitely many such $A$-steps,
% so eventually we reach another $R$-step.
% Repeating this gives the required infinite $R$-chain, with the given
% property.
% \qed
% \end{proof}

% This next proof approximates more closely to the Isabelle proof.
% \begin{proof}
% Assume that $A$ is well-founded.
% Define $R^-$ to be $R$, but excluding steps of the form $(w, z)$
% where there exists some $y$ such that $(y, z) \in A$ and $y$ is immortal.
% Assume that $R^-$ is well-founded.

% Suppose that there is an infinite descending $A \cup R$-chain.
% Choose a head $z$ of such a chain, choosing $z$ to be $A$-minimal,
% and also to be $R^-$-minimal among $A$-minimal immortal elements.
% As $z$ is $A$-minimal,
% the first step of an infinite chain must be (say) $(y, z) \in R$,
% and also in fact $(y, z) \in R^-$.
% As $A$ is well-founded,
% let $y$ be $A$-minimal among possible choices for $y$.
% Then, by the $R^-$-minimality of $z$, although $y$ is immortal, 
% it is not $A$-minimal among immortal members.
% So we have $(x, y) \in A$, where $x$ is immortal. 
% So as $R \circ A \subseteq (A \circ (A \cup R)^*) \cup R$, 
% we could replace $z >_R y >_A x$ in the infinite chain by 
% \begin{itemize}
% \item $(x, z) \in A \circ (A \cup R)^*$,
% say $(x, y') \in (A \cup R)^*$ and $(y', z) \in A$
% (where $x, y'$ and $z$ are immortal),
% but this would contradict the $A$-minimality of $z$ 
% (and our consequent inference that $(y, z) \not\in A$), or
% \item $(x, z) \in R$, which would contradict our choice of $y$
% which was to be $A$-minimal, since $x$ could have been chosen instead of $y$.
% \end{itemize}
% Thus, either way we get a contradiction, so $A \cup R$ is well-founded.
% \qed
% \end{proof}

% \begin{verbatim}
% wfp_tri_lem_dvk:
%    "[| dvk_cond ?R ?A; wf ?A;
%          wf (?R Int {(y, z). z ~: ?A `` (- wfp (?A Un ?R))}) |]
%       ==> ?x : wfp (?A Un ?R)" 
% \end{verbatim}

% Define $C^-$ to be $C$, but excluding steps of the form $(w, z)$
% where there exists some $y$ such that $(y, z) \in A$ and
% $y$ is $X \cup B \cup C$-immortal.

% For the purposes of Theorem~\ref{d-th3} $X$ will be $A$, 
% but we will use the lemma with more general $X$ when there are
% four or more relations.


% \section{The General Result }

% We use \texttt{dvk\_cond} $R\ A$,
% the condition from Doornbos \& von Karger \cite{dvk},
% that $R \circ A \subseteq (A \circ (A \cup R)^*) \cup R$

% \begin{verbatim}
% dvk_cond_def':
%   "dvk_cond ?s ?r == ?s O ?r <= (?r O (?r Un ?s)^*) Un ?s"
% \end{verbatim}


% We separate Dershowitz's proof into a number of lemmas.
% Note how, generally, statements in the proof of the form
% ``there exists an infinite chain'' have to be translated into a lemma
% with hypotheses and conclusion that certain relations are well-founded,
% or that something is in the well-founded part or a relation.  

% The \emph{well-founded part} (\texttt{wfp} in Isabelle)
% of a relation is the set whose elements 
% are not the head of any infinite descending chain.
% So a relation is well-founded if and only if 
% every member of the underlying set is in its well-founded part.

\begin{definition}[immortal]
Following Dershowitz, an \emph{$R$-immortal} element is the head of
an infinite descending $R$-chain
and ``\emph{immortal}'' means $(A \cup R)$-immortal, or
$(A \cup B \cup C)$-immortal, as the case may be.\marginpar{JED,
  please can you tidy this up. We really need to give the complicated
  Int part a name.
  I suggest just one definition for immortal, parametrized by the relation}
\begin{verbatim}
immortal_def:    "immortal R ?y == (?y : (- wfp ?R))"

Should we also define the A-image of R-immortal elements ??, ie
not sure if it's simplier, see altermative definition of cminus below

image_immortal_def: 
"image_immortal A R x == x : A `` {y : immortal R y}"
\end{verbatim}
\end{definition}

\begin{definition}\label{def:forward}
The (forward) \texttt{image} $r `` s$ of a set $s$ under a relation $r$ 
consists of those $z$ such that some $y \in s$ has $(y,z) \in r$.
\begin{verbatim}
Image_def: "?r `` ?s == {z. EX y:?s. (y, z) : ?r}"
\end{verbatim}
\end{definition}

In Definition~\ref{def:forward}, the expression \verb!y:?s! encodes
$x \in s$ and \verb!(y, z) : ?r! encodes $(y, z) \in r$ thus
in the next Definition~\ref{def:rminus}, \verb!~:! is $\not\in$. 


\begin{definition}[$R^-$]\label{def:rminus}
  \begin{eqnarray*}
    R^- & = & R \setminus \{(w, z) \mid \exists y. (y,z) \in A ~\&~ y
               \mbox{ is } (A \cup R)\mbox{-immortal }\}
\\
        & = & R \setminus \{(w, z) \mid \exists y. (y,z) \in A ~\&~ arimm ~y\}
\\
        & = & R \setminus \{(w, z) \mid \exists y. (y,z) \in A ~\&~ y
              \in (- wfp (A \cup R))\}
\\
        & = & R \cap \{(w, z) \mid z \not\in (A``(- wfp (A \cup R)))\}
  \end{eqnarray*}
\begin{verbatim}
 rminus ?R ?A == 
       (?R Int {(w, z). z ~: ?A `` (- wfp (?A Un ?R))})
\end{verbatim}
\end{definition}

Thus $R^-$ excludes from $R$ all steps of the form $(w, z)$ where
there exists some $y$ such that $(y, z) \in A$ and $y$ is $(A \cup
R)$-immortal.

\begin{lemma}[\texttt{wfp\_tri\_lem\_ch\_contra}] \label{lem-ch-contra}
  If $A \cup R^-$ is well-founded then $A \cup R$ is
  well-founded.
\begin{verbatim}
wfp_tri_lem_ch:
   "?x : wfp (?A Un (rminus ?R ?A)) ==> ?x : wfp (?A Un ?R)" 
\end{verbatim}
% \begin{verbatim}
% wfp_tri_lem_ch:
%    "?x : wfp (?A Un ?R Int {(y, z). z ~: ?A `` (- wfp (?A Un ?R))})
%       ==> ?x : wfp (?A Un ?R)" 
% \end{verbatim}
\end{lemma}
\begin{proof}
We can construct an infinite descending $(A \cup R)$-chain
using $A$ where possible and using $R$ only where necessary.
\qed
\end{proof}

\begin{corollary}[\texttt{wfp\_tri\_lem\_ch}] \label{lem-ch}
If there is an infinite descending $(A \cup R)$-chain 
then there is an infinite descending $(A \cup R)$-chain
where each step $(w, z) \in R$ in that chain
has the property that there is no $(y,z) \in A$ such that
$y$ is the head of an infinite descending $(A \cup R)$-chain.
\end{corollary}

\begin{lemma}[\texttt{wfp\_tri\_lem\_dvk\_contra}]\label{lem-dvk-contra}
If $R$ and $A$ satisfy the Doornbos \& von Karger \cite{dvk} condition 
\texttt{dvk\_cond}, and $A$ and $R^-$
are well-founded, then $A \cup R$ is well-founded.
\begin{verbatim}
wfp_tri_lem_dvk: "[| dvk_cond ?R ?A;  
       wf ?A; wf (rminus ?R ?A) |] ==> ?x : wfp (?A Un ?R)" 
\end{verbatim}
% \begin{verbatim}
% wfp_tri_lem_dvk:
%    "[| dvk_cond ?R ?A; wf ?A;
%        wf (?R Int {(y, z). z ~: ?A `` (- wfp (?A Un ?R))}) |]
%     ==> ?x : wfp (?A Un ?R)" 
% \end{verbatim}
\end{lemma}

We first give a more intuitive proof, then a proof which more closely
approximates the Isabelle proof.

\noindent\textit{Intuitive Proof.}
Consider an infinite descending $(A \cup R)$-chain.  
As $A$ is well-founded, from any point in this chain there must be another
$R$-step.
Wherever possible replace an $R$-step $z >_R v$ 
followed by an $A$-step $v >_A u$
by an $A$-step (possibly followed by a number of $A$- or $R$-steps)
in the given chain.
(This relates to the part 
$R \circ A \subseteq (A \circ (A \cup R)^*) \cup \ldots$
of \texttt{dvk\_cond}).
Alternatively, if possible, replace the remainder of the chain from this
point by any other infinite chain $z >_A y >_{A \cup R} \ldots$.
Again, this will not always be possible since $A$ is well-founded.

So, where this is not possible, we can
replace an $R$-step followed by an $A$-step by a single $R$-step,
which is possible using the part 
$R \circ A \subseteq \ldots \cup R$ of \texttt{dvk\_cond}.

Doing this repeatedly could absorb any number of $A$-steps, but, again,
as $A$ is well-founded there cannot be infinitely many such $A$-steps,
so eventually we reach another $R$-step.
Repeating this gives the required infinite $R$-chain, with the given
property.

The next proof approximates more closely to the Isabelle proof.
\begin{proof}
Assume that $A$ is well-founded.
Define $R^-$ to be $R$, but excluding steps of the form $(w, z)$
where there exists some $y$ such that $(y, z) \in A$ and $y$ is immortal.
Assume that $R^-$ is well-founded.

Suppose that there is an infinite descending $(A \cup R)$-chain.
Choose a head $z$ of such a chain, choosing $z$ to be $A$-minimal,
and also to be $R^-$-minimal among $A$-minimal immortal elements.
As $z$ is $A$-minimal,
the first step of an infinite chain must be $(y, z) \in R$ (say),
and also in fact $(y, z) \in R^-$.
As $A$ is well-founded,
let $y$ be $A$-minimal among possible choices for $y$.
Then, by the $R^-$-minimality of $z$, although $y$ is immortal, 
it is not $A$-minimal among immortal members.
So we have $(x, y) \in A$, where $x$ is immortal. 
Since $R \circ A \subseteq (A \circ (A \cup R)^*) \cup R$, 
we could replace $z >_R y >_A x$ in the infinite chain by 
\begin{description}
\item[\rm $(x, z) \in A \circ (A \cup R)^*$:]
say $(x, y') \in (A \cup R)^*$ and $(y', z) \in A$
where $x, y'$ and $z$ are immortal.
But this would contradict the $A$-minimality of $z$ 
and our consequent inference that $(y, z) \not\in A$, or
\item[\rm $(x, z) \in R$:] which would contradict our choice of $y$
which was to be $A$-minimal, since $x$ could have been chosen instead of $y$.
\end{description}

Thus, either way we get a contradiction, so $A \cup R$ is well-founded.
\qed
\end{proof}

\begin{corollary}[\texttt{wfp\_tri\_lem\_dvk}]\label{cor-dvk}
If $R$ and $A$ satisfy the Doornbos \& von Karger \cite{dvk} condition 
\texttt{dvk\_cond}, and $A$ is well-founded, 
and there is an infinite descending $(A \cup R)$-chain,
then there is an infinite descending $R$-chain
whose members are not of the form $z$ where $(y,z) \in A$ and
$y$ is immortal, ie is the head of an infinite descending 
$(A \cup R)$-chain.
\end{corollary}

% \begin{corollary}[Tripartite]
% The union $\stack{A\\B\\C}$ is well-founded if
% \begin{eqnarray}
% \stack{B\\C} A  & \subseteq & A\stack{A\\B\\C}^* \cup B \cup C\\\nonumber
% CB  & \subseteq & A\stack{A\\B\\C}^* \cup BB^* \cup C \;.
% \end{eqnarray}
% \end{corollary}

\begin{definition}
Define $C^-$ to be $C$, but excluding steps of the form $(w, z)$
where there exists some $y$ such that $(y, z) \in A$ and
$y$ is $(X \cup B \cup C)$-immortal.\marginpar{JED, we need to give
  the complicated Int construct a name.}
\begin{eqnarray*}
C^- & = & C \setminus \{(w, z) \mid \exists y. (y,z) \in A ~\&~ 
y \mbox{ is } (X \cup B \cup C)\mbox{-immortal} \}
\\
    & = & C \cap \{(w, z) \mid z \not\in  A``(- wfp (X \cup B \cup C)) \}
\end{eqnarray*}
\begin{verbatim}
  cminus ?C ?B ?A ?X == 
       (?C Int {(w, z). z ~: ?A `` (- wfp (?X Un ?B Un ?C))})

  cminus ?C ?B ?A ?X == 
       (?C Int {(w, z). ~ image_immortal A (X Un B Un C) z})

\end{verbatim}
\end{definition}

For the purposes of Theorem~\ref{d-th3}, $X$ will be $A$, 
but we will use the lemma with more general $X$ when there are
four or more relations.

\begin{lemma}[\texttt{wf\_tri\_lem\_BCm}]\label{lem-BCm}
If $B$ and $C^-$ 
are well-founded, 
and condition (\ref{d-th3-2}) of Theorem~\ref{d-th3} is satisfied, 
then $B \cup C^-$ is well-founded.\marginpar{JED please fix this. DONE}
\begin{verbatim}
wf_tri_lem_BCm: "[| wf ?B; wf (cminus ?C ?B ?A ?X);
 ?C O ?B <= (?A O (?X Un ?B Un ?C)^*) Un (?B O ?B^*) Un ?C |]
 ==> wf (?B Un (cminus ?C ?A ?B ?X))"
\end{verbatim}
% \begin{verbatim}
% wf_tri_lem_BCm: "[| ?BC = ?B Un ?C; wf ?B; 
%  ?C O ?B <= (?A O (?X Un ?BC)^*) Un (?B O ?B^*) Un ?C;
%  wf (?C Int {(y, z). z ~: ?A `` (- wfp (?X Un ?BC))}) |] 
%  ==> 
%  wf (?B Un ?C Int {(y, z). z ~: ?A `` (- wfp (?X Un ?BC))})"
% \end{verbatim}
\end{lemma}

\begin{proof}
Assume that $B$ and $C^-$ are well-founded.

For a contradiction, suppose that $B \cup C^-$ is not well-founded.
So there exists an $(B \cup C^-)$-immortal $z$.
Choose $z$ to be $B$-minimal such,
and also to be $C^-$-minimal among possible $B$-minimal choices.

As $z$ is $B$-minimal, the first step
of an infinite $B \cup C^-$-chain must be $(y, z) \in C^-$ (say).
As $B$ is well-founded,
let $y$ be $B$-minimal among possible choices for $y$.
Then, by the $C^-$-minimality of $z$, although $y$ is $(B \cup C^-)$-immortal,
it is not $B$-minimal among $(B \cup C^-)$-immortal members.
So we have $(x, y) \in B$, where $x$ is $(B \cup C^-)$-immortal. 
Since $C \circ B \subseteq (A \circ (X \cup B \cup C)^*) \cup
  (B \circ B^*) \cup C$, 
we could replace $z >_C y >_B x$ in the infinite chain by 
\begin{description}
\item[\rm $(x, z) \in A \circ (X \cup B \cup C)^*$:]
say $(x, y') \in (X \cup B \cup C)^*$ and $(y', z) \in A$ ---
but $x$ is $(B \cup C^-)$-immortal,
and so is the head of an infinite descending
$X \cup B \cup C$-chain, contradicting that $(y, z) \in C^-$; or
\item[\rm $(x, z) \in B \circ B^*$:]
  which would contradict our choice of $z$ to be $B$-minimal; or
\item[\rm $(x, z) \in C$:] and so $(x, z) \in C^-$ 
  which would contradict our choice of $y$ to be $B$-minimal,
  since $x$ could have been chosen instead of $y$.
\end{description}

Thus, in each case we get a contradiction, so $B \cup C^-$ is
well-founded.  \qed
\end{proof}

\renewcommand\theenumi{\alph{enumi}}
\renewcommand\labelenumi{(\theenumi)}

\begin{theorem}[\texttt{wf\_tri'}, Tripartite, Dershowitz, Theorem~3]
\label{d-th3}
Given three binary relations $A,B$ and $C$,
their tripartite union $A \cup B \cup C$ is well-founded if
all of the following hold:
\begin{quote}
\begin{enumerate}
\item\label{wff-ABC} each of $A, B, C$ are well-founded;
\item\label{disbunc} $D = (B \cup C)$;
\item\label{dvk-A-BC} $dvk\_cond ~D~ A$ ;
% $D \circ A \subseteq (A \circ (A \cup D)^*) \cup D$;
% \item\label{dvk-A-BC} $(B \cup C) \circ A \subseteq 
%   (A \circ (A \cup B \cup C)^*) \cup (B \cup C)$ where
\item\label{d-th3-2} $C \circ B \subseteq 
  (A \circ (A \cup D)^*) \cup (B \circ B^*) \cup C$.
\end{enumerate}
\end{quote}
\begin{verbatim}
wf_tri':  "[| 
    wf ?A ; wf ?B ; wf ?C ; 
    ?D = ?B Un ?C ; 
    dvk_cond ?D ?A ;
    ?C O ?B <= (?A O (?A Un ?D)^*) Un (?B O ?B^*) Un ?C
    |] ==> wf (?A Un ?D)"
CURRENT VERSION FOLLOWS
wf_tri';
  "[| ?BC = ?B Un ?C; dvk_cond ?BC ?A;
   ?C O ?B <= (?A O (?A Un ?BC)^*) Un (?B O ?B^*) Un ?C;
   wf ?A; wf ?B; wf ?C |] ==> wf (?A Un ?BC)" 
VERSION WITH BC and dvk_cond expanded FOLLOWS
wf_tri;
   "[| ?B Un ?C O ?A <= (?A O (?A Un (?B Un ?C))^*) Un (?B Un ?C);
    ?C O ?B <= (?A O (?A Un (?B Un ?C))^*) Un (?B O ?B^*) Un ?C;
    wf ?A; wf ?B; wf ?C |] ==> wf (?A Un (?B Un ?C))" 
\end{verbatim}
\end{theorem}

\begin{proof} \emph{(of Theorem~\ref{d-th3})}
By Corollary~\ref{cor-dvk} it is enough to prove 
that $(B \cup C)^-$ is well-founded.
By Lemma~\ref{lem-BCm} we have that $B \cup C^-$ is well-founded,
and clearly $(B \cup C)^- \subseteq B \cup C^-$.
\qed
\end{proof}

\section{Quatro-partite Well-foundedness}

Now we show how to extend this result to four (or more) relations.

\renewcommand\theenumi{\alph{enumi}}
\renewcommand\labelenumi{(\theenumi)}

\begin{theorem}[\texttt{wf\_four} Dawson and Gor\'e]
\label{th-four}
$Uall = A \cup B \cup C \cup D$ is well-founded if
\begin{enumerate}
\item each of $A,B,C$ and $D$ are well-founded, and 
\item \label{dvk-A-BCD} $(B \cup C \cup D) \circ A \subseteq 
  (A \circ (A \cup B \cup C \cup D)^*) \cup (B \cup C \cup D)$
\item \label{c-th3-DC} $D \circ C \subseteq 
  (A \circ (A \cup B \cup C \cup D)^*) \cup (C \circ C^*) \cup D$
\item \label{c-th3-DCB} $(C \cup D) \circ B \subseteq 
  (A \circ (A \cup B \cup C \cup D)^*) \cup (B \circ B^*)
    \cup C \cup D$
\end{enumerate}
\begin{verbatim}
val wf_four =
 "[| ?uall = ?A Un ?B Un ?C Un ?D; 
     wf ?A; wf ?B; wf ?C; wf ?D ;
     dvk_cond (?B Un ?C Un ?D) ?A;
     ?D O ?C <= (?A O ?uall^*) Un (?C O ?C^*) Un ?D;
     (?C Un ?D) O ?B <= (?A O ?uall^*) Un (?B O ?B^*) Un (?C Un ?D)
  |] ==> wf ?uall" 
\end{verbatim}
\end{theorem}

\begin{proof} 
We adapt the previous definition of $R^-$ for a relation $R$:
that is, $R^-$ is $R$, but excluding steps of the form $(w, z)$
where there exists some $y$ such that $(y, z) \in A$ and
$y$ is $(A \cup B \cup C \cup D)$-immortal:
\[
R^- = R \setminus \{(w, z) \in R \mid
\exists y. (y, z) \in A \mbox{ and }
y \mbox{ is } (A \cup B \cup C \cup D)-\mbox{immortal}\}.
\]

As $D$ is well-founded, \emph{a fortiori} $D^-$ is well-founded.
%
Setting $A,X,B,C$ to $A, A \cup B, C, D$, respectively, in
Lemma~\ref{lem-BCm} and using condition (\ref{c-th3-DC}), we obtain
that $C \cup D^-$ is well-founded, and so \emph{a fortiori}
$(C \cup D)^-$ is well-founded.
%
Setting $A,X,B,C$ to $A, A, B, C \cup D$, respectively in
Lemma~\ref{lem-BCm} and condition (\ref{c-th3-DCB}) we obtain that 
$B \cup (C \cup D)^-$ is well-founded and so \emph{a fortiori}
$(B \cup C \cup D)^-$ is well-founded.
%
Finally, by Corollary~\ref{cor-dvk} $A \cup B \cup C \cup D$ is well-founded.
\qed
\end{proof}

\section{The General Result}

We now extend Theorem~\ref{th-four} to an arbitrary number of relations.
The proof is straightforward but we need to set up some definitions.

First the condition we call \texttt{tri\_cond}, which is the condition 
satisfied by the list $[B,C,D]$ in the case of four relations.
It is defined recursively and gives (for example) conditions 
(\ref{c-th3-DC}) and (\ref{c-th3-DCB}) of Theorem~\ref{th-four}.

\newcommand{\bop}{\mathit{f}}

\begin{definition}\label{sec:foldr}
  For an arbitrary binary operator $\bop$, define the right-fold
  operator for list $[B,C,D]$ with initial value $Z$ to be
\[
 \mbox{foldr}~\bop~[B,C,D]~Z = B ~\bop~ (C ~\bop~ (D ~\bop~ Z))
\]
\begin{verbatim}
foldr.simps : [
   "foldr ?f [] ?z = ?z",
   "foldr ?f (?x # ?xs) ?z = ?f ?x (foldr ?f ?xs ?z)"] 
\end{verbatim}

\end{definition}

\begin{definition}\label{sec:general-result-tri}
  For all \verb!Auall!, the condition
  \texttt{tri\_cond Auall L} is true if
  \begin{description}
  \item[\rm Base Case:] L is the empty list
  \item[\rm Inductive Case:]  L=B.Bs and 
  $\mathtt{uBs} = \bigcup_{b \in \mathtt{Bs}} b$
  and
  $\mathtt{uBs \circ B \subseteq Auall \cup (B \circ B^*) \cup uBs}$
  and
  \texttt{tri\_cond Auall Bs} holds.
  \end{description}
\begin{verbatim}
tri_cond_Nil  : "tri_cond ?Auall [] = True"
tri_cond_Cons : "tri_cond ?Auall (?B # ?Bs) =
   ((let uBs = foldr (op Un) ?Bs {} 
      in uBs O ?B <= ?Auall Un (?B O ?B^*) Un uBs) 
   & tri_cond ?Auall ?Bs)"
\end{verbatim}
\end{definition}


We then need a separate lemma which is proved by structural induction on the 
list, say $[B,C,D]$, of relations.
For the general case we work with a list $B_1, B_2, \ldots, B_n$.

\begin{definition}
Define $U^-$ to be $U$, but excluding steps of the form $(w, z)$
where there exists some $y$ such that $(y, z) \in A$ and
$y$ is $(X \cup U)$-immortal:
\[
U^- = U \setminus \{(w, z) \in U \mid
\exists y. (y, z) \in A \mbox{ and }y \mbox{ is } (X \cup
U)\mbox{-immortal } \}
\]
\end{definition}

\begin{lemma} \label{lem-tri-n}
If $Bs = [B_1, B_2, \ldots, B_n]$,
and $B_1, B_2, \ldots, B_n$ are all well-founded, 
and $U = (B_1 \cup B_2 \cup \ldots \cup B_n)$
and
\texttt{tri\_cond} $A \circ (X \cup U)~~[B_1, B_2, \ldots, B_n]$ holds
then $U^-$ is well-founded.
\begin{verbatim}
tri_n_lem : 
 "[| ALL B:(set ?Bs) . wf B ; 
     ?uBs = foldr (op Un) ?Bs {}; 
     ?Auall = ?A O (?X Un ?uBs)^*;
     tri_cond ?Auall ?Bs |] ==> wf (uminus ?uBs ?A ?X)"
\end{verbatim}
\end{lemma}

\begin{proof}
The proof is by structural induction on the list 
$Bs = [B_1, B_2, \ldots, B_n]$.
That is, the base case is when $Bs$ is the empty list $[]$ and the
inductive step is when 
$Bs = [B_i, B_{i+1}, \cdots , B_n]$ 
and $X$ is an arbitrary $X_i$
and then the inductive hypothesis
used is that the lemma holds for 
$Bs = [B_{i+1}, \cdots , B_n]$ and
$X = X_i \cup B_i$.
The inductive step is  proved using 
Lemma~\ref{lem-BCm}.

The value used for $X$ varies throughout, so if its final value is $X_f$,
then the lemma is proved successively for 
\begin{align*}
& [] & X &= X_f \cup B_1 \cup B_2 \cup \ldots \cup B_n \\
& [B_n] & X &= X_f \cup B_1 \cup B_2 \cup \ldots \cup B_{n-1} \\
& \vdots & & \vdots \\ 
& [B_2, \ldots, B_n] & X &= X_f \cup B_1 \\
& [B_1, B_2, \ldots, B_n] & X &= X_f 
\end{align*}

Note that the value of $X \cup U$ (as used in the definition of $U^-$ above) 
therefore remains unchanged, and that at each step we also use,
in addition to Lemma~\ref{lem-BCm}, the fact that
if $B \cup V^-$ is well-founded, then $(B \cup V)^-$ is well-founded.
\qed
\end{proof}

Then we have the following theorem.

\begin{theorem}[Dawson and Gor\'e]
  Assuming that 
  $Bs = [B_1, B_2, \ldots , B_n]$, for $n \geq 1$, the union
  $A \cup B_1 \cup B_2 \cup \ldots \cup B_n$ is
  well-founded if
  \begin{enumerate}
  \item $A$ and $B_1, B_2, \ldots, B_n$ are all well-founded; and
%  \item $Bs = [B_1, B_2, \ldots , B_n]$;
  \item $U = (B_1 \cup B_2 \cup \ldots \cup B_n)$; and
  \item \texttt{tri\_cond}
  $A \circ (A \cup U)$ $[B_1, B_2, \ldots, B_n]$ holds; and
  \item $U \circ A \subseteq (A \circ (A \cup U)^*) \cup U$
  \end{enumerate}
\begin{verbatim}
tri_n "[| 
  wf ?A;  ALL B : (set ?Bs). wf B
  ?uBs = (foldr (op Un) ?Bs {}); 
  ?Auall = ?A O (?A Un ?uBs)^*; tri_cond ?Auall ?Bs; 
  dvk_cond ?uBs ?A |] ==> wf (?A Un ?uBs)" 
\end{verbatim}
\end{theorem}

\begin{proof}
By Lemma~\ref{lem-tri-n} we get that $U^-$ is well-founded, where 
we use $X = A$ in the definition of $U^-$.
Then Corollary~\ref{cor-dvk} gives the result.
\qed
\end{proof}

\bibliographystyle{plain}
\bibliography{tripartite}

\end{document}

