\documentclass{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{color}
\usepackage{natbib}
\usepackage{url}
\usepackage{bussproofs}
\usepackage{listings}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]

% \usepackage{exptrees}

\newcommand\comment[1]{} 

\renewcommand*\ttdefault{txtt}
\renewcommand{\qedsymbol}{$\dashv$}

\newcommand\MD{\ensuremath{\mathcal D}}
\newcommand\MS{\ensuremath{\mathcal S}}
\newcommand\MP{\ensuremath{\mathcal P}}
\newcommand\MQ{\ensuremath{\mathcal P}}
\newcommand\MC{\ensuremath{\mathcal C}}
\newcommand\MR{\ensuremath{\mathcal R}}
\newcommand\M{\ensuremath{\mathcal M}}

\newcommand\psl{\ensuremath\MQ_{l1} \ldots \MQ_{ln}}
\newcommand\psr{\ensuremath\MQ_{r1} \ldots \MQ_{rm}}

\newcommand{\Boxes}{\ensuremath{\vec{\Phi}}}
\newcommand{\Boxesi}[1]{\ensuremath{\vec{\Phi}_{-#1}}}
\newcommand{\cut}{cut-elimination}
\newcommand{\cuta}{cut-admissibility}
\newcommand{\ctra}{contraction-admissibility}
\newcommand{\weaka}{weakening-admissibility}

\lstset{language=ML,
        basicstyle=\ttfamily\small,
        showstringspaces=false,
        commentstyle=\itshape\color{blue},
        %frame=single,
        morekeywords={bind_thm,consts,inductive,qed_goal,defs}
       }

\begin{document}

\title{Structural Rule Admissibility for S4 and S4.3}

\author{Jesse Wu}

\maketitle

\input{jesse-intro}
\input{s4}
\input{s43}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
