% !TEX TS-program = latex
\documentclass[12pt]{beamer}
\usetheme[progressbar=frametitle]{metropolis}
\usepackage{appendixnumberbeamer}
\usepackage{booktabs}
\usepackage[scale=2]{ccicons}
\usepackage{pgfplots}
\usepgfplotslibrary{dateplot}
\usepackage{xspace}
\newcommand{\themename}{\textbf{\textsc{metropolis}}\xspace}
\pagestyle{empty}
\usepackage{latexsym,amssymb,mathdots}
\usepackage{ellipsis,multirow}
\usepackage{versions}\excludeversion{ignore}\excludeversion{comment}
\usepackage[dvipsnames,svgnames,xcolor=pst]{pstricks}
\usepackage{pst-node,pst-tree}
\newcommand{\olive}{\color{green}}
\newcommand{\azure}{\color{blue}}
\newcommand{\purple}{\color{violet}}
\newcommand{\bordeaux}{\color{red}}
\newcommand{\bA}{{\blue A}}
\newcommand{\rB}{{\red B}}
\newcommand{\pE}{{\purple E}}
\newcommand{\dn}[2]{\dotnode[dotscale=2,linecolor=yellow](#1){#2}}
\newcommand{\aA}[2]{\nccurve[linewidth=2pt,linecolor=red,linestyle=solid,angleA=0,angleB=180]{->}{#1}{#2} } %\naput*[npos=0.5]{\red$A$}}
\newcommand{\aB}[2]{\nccurve[linewidth=2pt,linecolor=blue,linestyle=dashed,angleA=0,angleB=180]{->}{#1}{#2} } %\nbput*[npos=0.5]{\blue$B$}}
\newcommand{\cA}{\pscircle[linecolor=red,fillcolor=red,fillstyle=solid]{0.3}} %{\white$A$}}
\newcommand{\cB}{\pscircle[linecolor=blue,fillstyle=crosshatch*,fillcolor=blue]{0.5}} %{\white$B$}}
\newcommand{\cC}{\pscircle[linecolor=green,fillstyle=hlines*,hatchsep=2pt,fillcolor=green]{0.7}} %{\white$C$}}
\newcommand{\cD}{\pscircle[linecolor=violet,fillstyle=vlines*,fillcolor=violet]{0.9}} %{\white$D$}}
\renewcommand{\emptyset}{\varnothing}
\newcommand{\plus}{{\mbox{\tiny\rm +}}}
\newcommand{\one}{I\/} 
\newcommand{\rel}{\mathrel}
\sloppy
\renewcommand{\emph}[1]{{\red\it #1}}
\newcommand{\ra}{\rightarrow}
\newcommand{\dotdot}{\mathbin{..}}
%
\title{Well-Founded Unions}
\author{Jeremy Dawson \and Nachum Dershowitz \and Rajeev Gor\'e}
\date{IJCAR, July 2018}
\begin{document}
\maketitle

\section{\S 0:  Introduction}


\begin{frame}{Problem}
Under what ``combinatorial'' conditions
is the union of \emph{well-founded relations} sure to be well-founded?\pause

\bigskip
\emph{Well-founded}: No infinite forward chains

\[\scalebox{3}{$\red\ra\ra\ra\cdots$}\]
\end{frame}

\begin{frame}{Problem}
Under what ``combinatorial'' conditions
is the \emph{union} of well-founded relations sure to be well-founded?
\bigskip

\[\scalebox{3}{$\red\ra\blue\ra\green\ra\cdots$}\]
\end{frame}

\begin{ignore}{Collaborators}
\begin{itemize}
\item Jeremy Dawson
\item Rajeev Gor\'e
\end{itemize}
\end{ignore}

\begin{frame}{Collaborators}
\begin{center}
\includegraphics[scale=0.35,angle=90]{Australia_Map3.eps}
\end{center}
\end{frame}

\begin{frame}{Collaboration}
  \begin{description}[M]
  \item[N, 2009:] {\blue Dear Rajeev, please could you send me a copy    of \ldots}
  \item[N, 2015:] {\blue Dear Colleagues, as you have shown interest in \ldots}
  \item[Raj to Jeremy:] {\red Can you formalise this stuff that Nachum has sent?}
  \item[Jeremy to Raj:] {\red Sure, have done a lot of very similar stuff \ldots}
  \item[Raj to N:] {\red Jeremy has just worked out a positive result \ldots}
  \end{description}
\end{frame}

\begin{frame}{Ideas}
\begin{itemize}
\item Constriction: Plaisted [1985]
\item Quasi-Commutation: Bachmair \& D [1986]
\item Use Ramsey: Geser [1989]
\item Jumping: Doornbos, Backhouse \& van der Woude [1997] 
\item Formalization: Dawson \& Gor\'e [2004] 
\end{itemize}
\end{frame}

\section{\S 1:  Termination}

\begin{frame}{Problem}
When
is the union of well-founded relations also well-founded?

\bigskip
\emph{Well-founded}: No infinite forward chains

\[\scalebox{3}{$\red\ra\ra\ra\cdots$}\]\pause
\[\begin{pspicture}(0,0)(5,0)
\rput(0.2,0){\cA}
\rput(1.45,0){\cA}
\rput(2.7,0){\cA}
\rput(4.6,0){\scalebox{3}{$\red\cdots$}}
\end{pspicture}\]
\end{frame}

\begin{frame}{Red Line}
\begin{center}
\includegraphics[scale=0.35,angle=90]{Red.eps}
\end{center}
\end{frame}

\begin{frame}{Blue Line}
\begin{center}
\includegraphics[scale=0.35,angle=90]{Blue.eps}
\end{center}
\end{frame}

\begin{frame}{Two Lines}
\begin{figure}[t]
\begin{pspicture}(-1,-0.5)(10,3)
\psset{origin={0,0},linewidth=1.5pt,linecolor=red,linearc=0.85}
\psline{->}(2.1,-0)(3.9,-0)
\psline{->}(4.1,0)(5.9,0)
\psline{->}(6.1,-0)(7.9,-0)
\psline{->}(2.1,0.1)(2.9,0.8)
\psline{->}(3.1,1.0)(3.9,1.7)
\psline{->}(4.1,1.9)(4.9,2.6)
\psline{->}(4.1,0.1)(4.9,0.8)
\psline{->}(5.1,1.0)(5.9,1.7)
\psline{->}(6.1,0.1)(6.9,0.8)
\rput(8.5,0){$\cdots$}\rput(7,1.5){$\cdots$}\rput(5.3,3.1){$\iddots$}
\psset{linewidth=1.5pt,linecolor=blue,linestyle=dashed}
\psline{->}(3.1,0.8)(3.9,0.1)
\psline{->}(4.1,1.7)(4.9,1.0)
\psline{->}(5.1,0.8)(5.9,0.1)
\psline{->}(6.1,1.7)(6.9,1.0)
\psline{->}(7.1,0.8)(7.9,0.1)
\psline{->}(5.1,2.6)(5.9,1.9)
\rput(2,0){$\olive\bullet$}\rput(4,0){$\olive\bullet$}\rput(6,0){$\olive\bullet$}\rput(8,0){$\olive\bullet$}
\rput(3,0.9){$\olive\bullet$}\rput(5,0.9){$\olive\bullet$}\rput(7,0.9){$\olive\bullet$}
\rput(4,1.8){$\olive\bullet$}\rput(6,1.8){$\olive\bullet$}\rput(5,2.7){$\olive\bullet$}
\end{pspicture}
\end{figure}
\end{frame}

\begin{frame}{A to B}
\vspace*{-15mm}
\begin{center}
\includegraphics[scale=0.4]{Warhol.eps}
\end{center}
\end{frame}

\begin{frame}{A to B}
\begin{center}
\includegraphics[scale=0.27]{A2B.eps}
\end{center}
\end{frame}

\begin{frame}{Immortality}
\begin{itemize}
\item {\red Have pass for unlimited  Red travel}
\item {\blue Have pass for unlimited Blue travel}
\item Can't ride forever on just one
\item Want to ride forever on the combination
\end{itemize}
\end{frame}

\begin{frame}{Mortal Union}
\begin{center}
\begin{pspicture}(0,-0.8)(10,0.7)
\dn{0,0}{x}
\dn{2,0}{y}
\dn{4,0}{z}
\dn{6,0}{a}
\dn{8,0}{b}
\aA x y \aB y z \aA z a \aB a b
\end{pspicture}
\end{center}
\end{frame}

\begin{frame}{Immortal Union}

\begin{figure}[t]
\begin{pspicture}(0,-0.5)(10,1.0)
\psset{origin={0,0},linewidth=1.5pt,linecolor=red,linearc=0.85}
\psline{->}(2.1,-0.1)(3,-0.5)(3.9,-0.1)
\psline{->}(6.1,-0.1)(7,-0.5)(7.9,-0.1)
\rput(10.5,0){$\cdots$}
\psset{linewidth=1.5pt,linecolor=blue,linestyle=dashed}
\psline{->}(4.1,0)(5.9,0)
\psline{->}(8.1,0)(9.9,0)
\psline{<-}(2.1,0.1)(3,0.5)(3.9,0.1)
\psline{<-}(6.1,0.1)(7,0.5)(7.9,0.1)
\rput(2,0){$\olive\bullet$}\rput(4,0){$\olive\bullet$}\rput(6,0){$\olive\bullet$}\rput(8,0){$\olive\bullet$}\rput(10,0){$\olive\bullet$}
\end{pspicture}
\end{figure}
\end{frame}

\begin{frame}{Relations}
\[\scalebox{3}{$\red\ra\quad\blue\ra\quad\green\ra\quad\purple\ra\black\cdots$}\]
\pause

\begin{pspicture}(-0.5,0)(5,2)
\rput(0,0){\cA}
\rput(2.5,0){\cB}
\rput(5,0){\cC}
\rput(7.5,0){\cD}
\end{pspicture}
\end{frame}

\begin{frame}{Union}
\[
\begin{pspicture}(0,0)(0,0)
\rput(0,0){\cD}
\rput(0,0){\cC}
\rput(0,0){\cB}
\rput(0,0){\cA}
\end{pspicture}
\]
\end{frame}

\section{\S 2: Bipartite Case}

\begin{frame}{Must be Mixed}
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB\cA}
\rput(2,0){\cB\cA}
\rput(4,0){\cB\cA}
\rput(6,0){\cB\cA}
\rput(8,0){\cB\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
\only<2>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cA}
\rput(2,0){\cA}
\rput(4,0){\cA}
\rput(6,0){\cA}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\only<3>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cA}
\rput(2,0){\cB}
\rput(4,0){\cB}
\rput(6,0){\cB}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\only<4>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cA}
\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause\pause\pause
\end{frame}

\begin{frame}{Inversion}
\begin{pspicture}(-1,-2)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\end{pspicture}
\end{frame}

\begin{frame}{Trivial}
\begin{pspicture}(-1,-2)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(3,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(8,0){\cB}
\end{pspicture}
\pause

\only<2>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cA}
\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause
\only<3>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
%\rput(2,0){\cA}
\rput(4,0){\cA}
\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause
\only<4>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
%\rput(2,0){\cA}
%\rput(4,0){\cA}
\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause
\only<5>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
%\rput(2,0){\cA}
%\rput(4,0){\cA}
\rput(6,0){\cB}
%\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\end{frame}

\begin{frame}{Trivial Pursuit}
\begin{pspicture}(-1,-2)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(3,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(8,0){\cA}
\end{pspicture}
\pause

\only<2>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cA}
\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause

\only<3>{
\begin{pspicture}(-1,-1)(11,1)
%\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cA}
\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}

\pause
\only<4>{
\begin{pspicture}(-1,-1)(11,1)
%\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cA}
%\rput(6,0){\cB}
\rput(8,0){\cA}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}

\end{frame}

\begin{frame}{Easy Does It}
\begin{pspicture}(-1,-3)(11,2)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(3,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\only<1-5>{\rput(8,1){\cA}}
\rput(8,-1){\cB}
\end{pspicture}
\pause

\only<2>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cB}
\rput(6,0){\cA}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause

\only<3>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
\rput(2,0){\cA}
%\rput(4,0){\cB}
\rput(6,0){\cA}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause

\only<4>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
%\rput(2,0){\cA}
%\rput(4,0){\cB}
\rput(6,0){\cA}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
}
\pause

\only<5-6>{
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cB}
%\rput(2,0){\cA}
%\rput(4,0){\cB}
\only<5>{\rput(6,0){\cA}}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
\vspace*{-40mm}
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\only<5>{\psline{->}(-0.7,0.9)(2,0.2)(3.9,0.7)
\rput(1,0.3){X}}
\end{pspicture}
}
\pause
}
\end{frame}

\begin{frame}{Jumping}
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cB}
\rput(6,1){\cA}\rput(8,1){\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cB\cA}
\end{pspicture}

\pause
\begin{pspicture}(-1,-1)(11,2)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cB}
\rput(6,0){\cA}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}

\pause
%\vspace*{-20mm}
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\psline{->}(-0.7,0.9)(0,.4)(.7,0)
\psset{linecolor=red,linestyle=dotted}
\psline{->}(.7,0)(2,0.2)(3.9,0.7)
\psset{linecolor=blue,linestyle=dashed}
\psline{->}(.7,0)(2,0.2)(3.9,0.7)
\rput(0.5,0.3){X}
\end{pspicture}
}

\end{frame}

\begin{frame}{Counterexample}

\begin{pspicture}(-1,-1.5)(11,2)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(3,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(7.8,1){\cA}\rput(9,1){\cA}
\rput(7.8,-1){\cB}\rput(9,-1){\cB}
\end{pspicture}
\pause

\begin{center}
\scalebox{2}{
\begin{pspicture}(-1,-0.8)(5,0.5)
\psset{linewidth=1.5pt,linecolor=blue,linestyle=dashed,linearc=0.85,origin={-2.5,0}}
\dn{2,0}{x}
\dn{4,0}{x}
\dn{6,0}{x}
\psline{->}(2.1,-0.1)(3,-0.5)(3.9,-0.1)
\psline{->}(4.1,-0.1)(5,-0.5)(5.9,-0.1)
\psset{linecolor=red,linestyle=solid}
\psline{<-}(2.1,0.1)(4,0.5)(5.9,0.1)
\psline{->}(4.1,0)(5.9,0)\end{pspicture}
}
\end{center}
\end{frame}

\section{\S 3:  Tripartite}

\begin{frame}{Jumping $\times$ 2}
\psset{unit=7mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cB}
\rput(6,1){\cA}\rput(8,1){\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cB\cA}
\end{pspicture}

\bigskip
\bigskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cC}\rput(2,0){\cB\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cC}
\rput(6,1){\cB\cA}\rput(8,1){\cC\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB\cA}
\end{pspicture}
\end{frame}


\begin{frame}{2 $\times$ Jumping}
\psset{unit=7mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cC\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cC\cB}
\rput(6,1){\cA}\rput(8,1){\cC\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB\cA}
\end{pspicture}

\bigskip
\bigskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cC}\rput(2,0){\cB}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cC}
\rput(6,1){\cB}\rput(8,1){\cC\cB}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB}
\end{pspicture}
\end{frame}

\begin{frame}{Tripartite: Preference}
\psset{unit=7mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cC\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cC\cB}
\rput(6,1){\cA}\rput(8,1){\cC\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB\cA}
\end{pspicture}

\bigskip
\bigskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cC}\rput(2,0){\cB}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-3){\cC}
\rput(6,1){\cA}\rput(8,1){\cC\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB\cA}
\rput(6,-1){\cB}\rput(8,-1){\cB}\rput(9.5,-1){$\bullet\bullet\bullet$}\rput(11,-1){\cB}
\end{pspicture}
\end{frame}

\begin{frame}{Constriction}

\begin{pspicture}(-1,-1)(11,2)
\rput(0,0){\cB}
\rput(2,0){\cA}
\rput(4,0){\cB}
\rput(6,0){\cA}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
\pause
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\psline{->}(-0.7,0.9)(0,.4)(.7,0)
\psset{linecolor=red,linestyle=dotted}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=blue,linestyle=dashed}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\rput(0.5,0.3){X}
\end{pspicture}
}
\end{frame}

\begin{frame}{More Constriction}

\begin{pspicture}(-1,-1)(11,2)
\rput(0,0){\cB}
\rput(2,0){\cC}
\rput(4,0){\cB}
\rput(6,0){\cA}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
\pause
\only<2>{
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\psline{->}(-0.7,0.9)(0,.4)(.7,0)
\psset{linecolor=red,linestyle=dotted,dotsep=1pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=blue,linestyle=dotted,dotsep=2pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=green,linestyle=dotted,dotsep=3pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\rput(0.5,0.3){X}
\end{pspicture}
}}
\pause
\onslide<3>{
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\psline{->}(0.5,0.8)(.7,0)
\psset{linecolor=red,linestyle=dotted,dotsep=1pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=blue,linestyle=dotted,dotsep=2pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=green,linestyle=dotted,dotsep=3pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\rput(0.4,0.3){X}
\end{pspicture}
}}

\end{frame}

\begin{frame}{Tripartite}
\psset{unit=7mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cC\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-1){\cC\cB}
\only<1>{\rput(6,1){\cA}\rput(8,1){\cC\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB\cA}}
\end{pspicture}
\pause
\end{frame}

\begin{frame}{Constriction}

\begin{pspicture}(-1,-1)(11,2)
\rput(0,0){\cB}
\rput(2,0){\cC}
\rput(4,0){\cB}
\only<1-2>{\rput(6,0){\cA}}
\rput(8,0){\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}

\pause
\only<2>{
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\psline{->}(1.2,0.8)(.7,0)
\psset{linecolor=red,linestyle=dotted,dotsep=1pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=blue,linestyle=dotted,dotsep=2pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\psset{linecolor=green,linestyle=dotted,dotsep=3pt}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\rput(1.2,0.4){X}
\end{pspicture}
}}
\pause

\end{frame}

\begin{frame}{Even More Constriction}

\begin{pspicture}(-1,-1)(11,2)
\only<1>{\rput(0,0){\cC\cB}}
\only<2>{\rput(0,0){\cC}}
\only<1>{\rput(2,0){\cC\cB}}
\only<2>{\rput(2,0){\cC}}
\only<1>{\rput(4,0){\cC\cB}}
\only<2>{\rput(4,0){\cB}}
\rput(6,0){\cC\cB}
\rput(8,0){\cC\cB}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
\pause

\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=blue,linestyle=solid}
\psline{->}(-0.7,0.9)(0,.4)(.7,0)
\psset{linecolor=blue,linestyle=dashed}
\psline{->}(.7,0)(2,0.2)(3.9,0.5)
\rput(0.4,0.4){X}
\end{pspicture}
}
\end{frame}

\begin{frame}{Tripartite}
\psset{unit=7mm}
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cC}\rput(2,0){\cB}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,-3){\cC}
\only<1>{\rput(6,1){\cA}\rput(8,1){\cC\cB\cA}\rput(9.5,1){$\bullet\bullet\bullet$}\rput(11,1){\cC\cB\cA}
\rput(6,-1){\cB}\rput(8,-1){\cB}\rput(9.5,-1){$\bullet\bullet\bullet$}\rput(11,-1){\cB}}
\end{pspicture}
\pause
\end{frame}

\begin{frame}{Even More Constriction}

\begin{pspicture}(-1,-1)(11,2)
\only<1>{\rput(0,0){\cC\cB}}
\only<2-3>{\rput(0,0){\cC}}
\only<1>{\rput(2,0){\cC\cB}}
\only<2>{\rput(2,0){\cB}}
\only<1>{\rput(4,0){\cC\cB}}
\only<2-3>{\rput(4,0){\cC}}
\only<1>{\rput(6,0){\cC\cB}}
\only<2>{\rput(6,0){\cB}}
\only<1>{\rput(8,0){\cC\cB}}
\only<2-3>{\rput(8,0){\cC}}
\rput(10,0){$\bullet~\bullet~\bullet$}
\end{pspicture}
\pause
\pause
\end{frame}

\begin{frame}{Counterexamples}
\begin{center}
\psset{arrowsize=1pt 3}
\only<1>{
\begin{pspicture}(-4,0)(4,2)
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=3pt,linecolor=red,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed,linearc=2]{->}(3.9,0.1)(3,1.5)(-2,1.5)(-3.9,0.1) % z->v
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=2]{->}(-0.9,0.1)(1.4,0.9) % x->y
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed,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}
}
\pause
\only<2>{
\begin{pspicture}(-4,0)(4,2)
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=3pt,linecolor=red,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed,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}
}
\pause
\only<3>{
\begin{pspicture}(-4,0)(4,2)
\psline[linewidth=3pt,linecolor=green,linestyle=dotted,linearc=4]{->}(-3.8,-0.1)(-1,-1.0)(1,-1)(3.9,-0.1) % v->z
\psline[linewidth=3pt,linecolor=blue,linestyle=dashed]{->}(-3.9,0)(-1.1,0) % v->x
\psline[linewidth=3pt,linecolor=red,linearc=2]{->}(-0.9,0)(1.5,-0.5)(3.7,0) % x->z
\psline[linewidth=3pt,linecolor=red,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}

\end{frame}

\section{\S 4:  Quadripartite}

\begin{frame}{Quadripartite: Preference}
\psset{unit=6mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cD\cC\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.3,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(12,0){\cD\cC\cB}
\end{pspicture}

\medskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cD\cC}\rput(2,0){\cB}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.5,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(11.7,0){\cB}\rput(13.2,0){\cB}\rput(14.2,0.5){\Huge\bf *}
\rput(15.5,0){\Huge\bf /}
\rput(17.,0){\cD\cC}
\end{pspicture}

\medskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cD}\rput(2,0){\cC}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.5,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(11.7,0){\cC}\rput(13.2,0){\cC}\rput(14.2,0.5){\Huge\bf *}
\rput(15.5,0){\Huge\bf /}
\rput(17.,0){\cD}
\end{pspicture}
\end{frame}

\begin{frame}{Generalized Constriction}
\begin{pspicture}(-1,-1)(11,2)
\rput(0,0){\cD\cC}
\end{pspicture}
\scalebox{2}{
\begin{pspicture}(-1,-2)(1,0.5)
\psset{linewidth=1.5pt,linearc=0.85}
\psset{linecolor=red,linestyle=solid}
\psline{->}(-0.4,0.7)(0,.4)(.7,0)
\psset{linecolor=black,linestyle=dashed}
\psline{->}(.7,0)(2,0.2)(3.9,-0.7)
\rput(0.5,0.4){X}
\end{pspicture}
}
\end{frame}

\begin{frame}{Induction}
\begin{pspicture}(-1,-1)(11,1)
\rput(0,0){\cD}
\rput(3,0){\cD\cC}
\rput(6,0){\cD\cC\cB}
\rput(9,0){\cD\cC\cB\cA}
\end{pspicture}
\end{frame}

\begin{frame}{Quadripartite: Preference \& Jumping}
\psset{unit=6mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cD\cC\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.3,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(12,0){\cD\cC\cB}
\end{pspicture}

\medskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cD\cC}\rput(2,0){\cB}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.5,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(11.7,0){\cB}\rput(13.2,0){\cB}\rput(14.2,0.5){\Huge\bf *}
\rput(15.5,0){\Huge\bf /}
\rput(17.,0){\cD\cC}
\end{pspicture}

\medskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cD}\rput(2,0){\cC}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cC}\rput(8,0){\cD\cC}\rput(9.5,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(11.7,0){\cD}
\end{pspicture}
\end{frame}

\begin{frame}{Quadripartite: Open}
\psset{unit=6mm}
\begin{pspicture}(0,-1)(11,1.5)
\rput(0,0){\cD\cC\cB}\rput(2,0){\cA}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.3,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(12,0){\cD\cC\cB}
\end{pspicture}

\medskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cD\cC}\rput(2,0){\cB}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cA}\rput(8,0){\cD\cC\cB\cA}\rput(9.5,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(11.7,0){\cB}\rput(13.2,0){\cB}\rput(14.2,0.5){\Huge\bf *}
\rput(15.5,0){\Huge\bf /}
\rput(17.,0){\cD\cC}
\end{pspicture}

\medskip
\begin{pspicture}(0,-1)(11,2)
\rput(0,0){\cD}\rput(2,0){\cC}
\rput(2.4,-1){\pspolygon*[linearc=.2,linecolor=black](1,0)(1,2)(3,1)}
\rput(6,0){\cB}\rput(8,0){\cD\cC\cB}\rput(9.5,0.5){\Huge\bf *}
\rput(10.5,0){\Huge\bf /}
\rput(11.7,0){\cC}\rput(13.2,0){\cC}\rput(14.2,0.5){\Huge\bf *}
\rput(15.5,0){\Huge\bf /}
\rput(17.,0){\cD}
\end{pspicture}
\end{frame}

\section{\S 5:  $n$-partite}

\begin{frame}{Main Theorem}

$R_{i : n} = R_i \cup \cdots \cup R_n $

\bigskip

$R_{0 : n} $ is well-founded if, for some $k$:
\begin{align*}
 R_{i+1 : n} R_i &\subseteq R_0 R_{0 : n}^\ast \cup R_i^\plus 
\cup R_{i+1 : n} &&\mbox{for } i=0\dotdot k-1 \\
R_{i+1 : n} R_i & \subseteq R_i R_{i : n}^\ast 
\cup R_{i+1 : n} &&\mbox{for } i=k\dotdot n-1 
\end{align*}
\end{frame}

\section{\S $\infty$: Morals}

\begin{frame}{Formalizing All Along}
  \begin{description}[M]
  \item[N:]  {\blue Here is a draft of some results}
  \item[Jeremy:] {\red Have formalised; all claims are correct}
  \item[N:] {\blue I'm stuck on this \dots}
  \item[Jeremy:] {\red So am I \dots}
  \item[Raj:] {\red Have you tried \dots}
  \item[Jeremy:] {\red No, but will try \dots. It works!}
  \item[N:]  {\blue Thanks, here are some variations}
  \item[Jeremy:] {\red Here are the proofs for your variations and some
    further generalisations}
  \item[Raj:] {\red My suggestion would be to try for IJCAR 2016}
  \end{description}
\end{frame}


\begin{frame}{Moral}
  \begin{description}[M]
  \item[IJCAR 2016:] \emph{``How to'' -- rejected} 
    \begin{enumerate}
    \item could not install Isabelle/HOL 2005
    \item using Isabelle/HOL 2005 is bad
    \item instructions are incomplete
    \end{enumerate}

%\pause
%  \item[CSL 2016:] ``how to'' -- rejected
\bigskip
\pause
  \item[IJCAR 2018:] \emph{Traditional paper -- accepted}

\bigskip 
  \pause
  \item[Moral:] 
\item[]  \begin{verse}Write traditionally and just say,\\ ``All proofs have been
    mechanically verified''\\
(icing on the cake)\end{verse}
  \end{description}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Isabelle/HOL 2005}
\scriptsize    \url{users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/tripartite-README}
\end{frame}

\begin{frame}{Scotland Law Reports [1878]}
Although we are not to decide\\ whether the reasons\\ against the {\red union}\\ are {\red well founded},\\ yet, far short of that,\\ in such a question \\there may be\\ fair grounds of objection.
\end{frame}

\end{document}
