\documentclass[a4paper,12pt]{llncs}
\frenchspacing
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{color}
\usepackage{array}
\usepackage{url}
%\usepackage{hyperref,breakurl}
\usepackage{versions}\excludeversion{ignore}
\usepackage{soul}\setstcolor{red}
%\usepackage{amssymb,amsthm,latexsym,amsmath,mathdots}
\usepackage{amssymb,latexsym,amsmath,mathdots}
\usepackage{epstopdf}
\usepackage[dvipsnames,svgnames]{pstricks}
\usepackage{fancyvrb}
\usepackage[all]{xy}
\usepackage{epigraph}
\pagestyle{plain}

%%% Jeremy's commands
%\newcommand{\frwd}[2]{#1 `` #2}
\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{\comp}[2]{#1 #2}
\newcommand{\comq}[2]{#1 \circ #2}
%\newcommand{\trun}[3]{\{#1 \!\mid\! #2 \!\mid\! #3\}}
\newcommand{\trun}[3]{(#1 \cup #2 \cup #3)} % {(#1 \!\cup\! #2 \!\cup\! #3)}
\newcommand{\trum}[3]{#1 \cup #2 \cup #3} % {#1 \!\cup\! #2 \!\cup\! #3}
%\newcommand{\biun}[2]{\{#1 \!\mid\! #2\}}
\newcommand{\biun}[2]{(#1 \cup #2)} % {(#1 \!\cup\! #2)}
%\newcommand{\biun}[2]{(#1 \cup #2)}
\newcommand{\trans}[1]{#1^{\ast}}
\newcommand{\bop}{\mathit{f}}

%%% 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}}
\let\rel=\mathrel
%\newcommand{\stack}[1]{{\def\\{|}{\{#1\}}}}
\newcommand{\stack}[1]{{\def\\{|}{\{#1\}}}}
\newcommand{\rstack}[1]{\rel{\stack{#1}}}
\newcommand{\ok}[1]{#1}
\newcommand{\nd}[1]{\begin{blue}#1\end{blue}}
%\newcommand{\rpg}[1]{\begin{green}#1\end{green}}
\newcommand{\rpg}[1]{#1}
\DefineVerbatimEnvironment{Isa}{Verbatim}{frame=single,fontshape=rm,fontsize=\small}
\newcommand{\plus}{{\scriptscriptstyle +}}
\newcommand{\dotdot}{\mathop{..}}
\newcommand{\nb}[1]{\marginpar{\small\red #1}}
\newcommand{\ig}[1]{}

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

\institute{
Research School of Computer Science, Australian National University
\and
School of Computer Science, Tel Aviv University 
\and
\ok{Institut d'\'etudes avanc\'ees de Paris}
}


\begin{document}
\sloppy
\section*{Finite Rearrangment}\label{sec:fin}

\begin{theorem}
Given preferential commutation:
$$B_{i+1\dotdot n}  B_i  \subseteq B_0  B_{0\dotdot n}^\ast  \cup B_i^+ \cup B_{i+1\dotdot n} \mbox{ for all } i=0\dotdot n-1$$
and given that each $B_i$ is well-founded.
we have that any chain in the union of the $B_i$ can be replaced by a sequence of $B_i$ steps with nondecreasing indices:
$$B_{0\dotdot n}^\ast  \subseteq B_0^\ast  B_1^\ast  \cdots B_n^\ast .$$
\end{theorem}
\noindent
Compare \cite[Thm.~54]{dershowitz-jumping}.

\begin{proof}
Suppose there is a chain $s \rel{B_{0\dotdot n}^\ast } t$ from $s$ to $t$.
We look for inversions and replace them.

Analogous to our previous use of constricting steps $B_i^-$, let $C_i$ be $B_i$ ($i\geq 1$)
with the constraint that there is no chain 
leading out of the source $u$ of a step $u \rel{B_i} w$ that begins with an $A=B_0$ step $u \rel{A} v$, continues with arbitrary $B=B_{0\dotdot n}$ steps and ends up at $t$.
That is,
$$u \rel{C_i} w \rel{B^\ast} t$$
if 
$$u \rel{B_i} w \rel{B^\ast} t$$
but there is no
$$u \rel{A} v \rel{B^\ast} t$$

Since $A$ is well-founded, we can construct a $B$ path that takes the preferred $A$ whenever it is  possible to do so and still arrive eventually at $t$.
That leaves us with a chain  $s \rel{(A \cup C)^\ast} t$,
where $C$ is short for $C_{1\dotdot n}$.
Any $B$-step taken is a constricted $C$-step.

We are given (for $i=0$) that
$$B_{1\dotdot n}  A  \subseteq A  B^\ast  \cup A^+ \cup B_{1\dotdot n}$$
which means that
$$C  A  \subseteq C$$
since, in this case, an initial $A$-step is precluded.
This implies that all the non-initial $A$-steps in  $s \rel{(A \cup C)^\ast} t$
can be erased, leaving $s \rel{A^\ast C^\ast } t$.

Consider again the preferential condition,
$$B_{i+1\dotdot n}  B_i  \subseteq A  B_{0\dotdot n}^\ast  \cup B_i^+ \cup B_{i+1\dotdot n}$$
This implies
$$C_{i+1\dotdot n}  B_i  \subseteq C_i B_i^\ast  \cup C_{i+1\dotdot n}$$
By an easy induction
$$C_{i+1\dotdot n}  B_i^\ast  \subseteq C_i B_i^\ast  \cup C_{i+1\dotdot n}$$
By another induction
$$(C_{i+1\dotdot n}  B_i^\ast)^\ast \subseteq  B_i^\ast C_{i+1\dotdot n}^\ast  $$
This is because
\begin{align*}
(C_{i+1\dotdot n}  B_i^\ast)(C_{i+1\dotdot n}  B_i^\ast)^\ast &\subseteq (C_i B_i^\ast  \cup C_{i+1\dotdot n}) B_i^\ast  C_{i+1\dotdot n}^\ast\\
&\subseteq C_i B_i^\ast  C_{i+1\dotdot n}^\ast \cup   (C_{i+1\dotdot n} B_i^\ast ) C_{i+1\dotdot n}^\ast\\
& \subseteq B_i^\ast C_{i+1\dotdot n}^\ast 
\end{align*}

Applying
$$(C_{i+1\dotdot n}  B_i^\ast)^\ast \subseteq  B_i^\ast C_{i+1\dotdot n}^\ast $$
repeatedly, for $i=1,\dots,n-1$, moves lower-indexed relations to the left and results in 
$$s \rel{A^\ast B_1^\ast B_2^\ast \cdots B_n^\ast} t$$
as claimed.
\qed\end{proof}

\nb{How much well-foundedness is actually needed?}

\bibliographystyle{splncsa}
\bibliography{tripartite}

\end{document}
