\documentclass[a4paper]{scrartcl}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{cite}
\usepackage{url}
\usepackage{eulervm}
\usepackage{version}
\usepackage{mathpartir}
\usepackage{alltt}
\usepackage{tcolorbox}

\title{COMP3161/9164 Homework Example}

% \date{}

\begin{document}

\maketitle

\newcommand{\M}{\mathbf{M}}
\newcommand{\J}{\mathbf{J}}
\newcommand{\EL}{\mathbf{L}}
\newcommand{\N}{\mathbf{N}}
\newcommand{\proofcase}[1]{\vspace{1ex}

\noindent\textbf{#1}}

\section{M/L/N Example}

Recall our language of matched parentheses
\[ \{ \epsilon, (), (()), ()(), \ldots \} \]

\noindent
This is the definition of $\M$:

\[
        \inferrule{ }{\varepsilon\ \M}{M_E} \quad \quad \quad
        \inferrule{ s\ \M }{\texttt{(}s\texttt{)}\ \M }{M_N}\quad\quad\quad
        \inferrule{ s_1\ \M \\ s_2\ \M}{ s_1s_2\ \M}{M_J}
\]

\noindent
This is the unambiguous definition of $\EL$ and $\N$:

\[
        \inferrule{ }{\varepsilon\ \EL}{L_E} \quad \quad \quad
        \inferrule{ s\ \EL }{\texttt{(}s\texttt{)}\ \N }{N_N}\quad\quad\quad
        \inferrule{ s_1\ \N \\ s_2\ \EL}{ s_1s_2\ \EL}{L_J}
\]

\noindent
This is the essential lemma $1$ in the proof that $\M$ is contained in $\EL$:

\[
        \inferrule{ s\ \EL \\ t\ \EL}{ st\ \EL}
\]

\section{Homework}

\subsection*{Prove Lemma 1}

This is my solution.

\proofcase{Goal:} 
We must show
$\forall ~s. ~ s\ \EL ~ \longrightarrow (\forall ~t. ~ t\ \EL ~ \longrightarrow ~ st\ \EL)$

We will prove this
by rule induction, proving $P(s)$ for all $s$ for which $s\ \EL$ is derivable and simultaneously
proving $Q(s)$ for all $s$ for which $s\ \N$ is derivable, where $P$ and $Q$ are defined by:

\[ P(s) \equiv ((\forall ~t. ~ t\ \EL ~ \longrightarrow ~ st\ \EL) ~ \wedge ~ s\ \EL) \]

\[ Q(s) \equiv s\ \N \]

We have three cases to show, corresponding to the three rules that define $\EL$ and $\N$.

\proofcase{Case 1:} The base case associated with rule $L_E$.

We must show $P(\epsilon) \equiv \epsilon\ \EL$.

This follows from $L_E$, as it is exactly the statement of $L_E$.

\proofcase{Case 2:} The inductive case associated with $L_J$.

We assume two inductive hypotheses, $IH_1 \equiv Q(s_1) \equiv s_1\ \N$ and $IH_2 \equiv P(s_2)$.

We must show $P(s_1s_2) \equiv (\forall ~t. ~ t\ \EL ~ \longrightarrow ~ s_1s_2t\ \EL) \wedge s_1s_2\ \EL$.

Let us prove the two conjuncts separately.

\proofcase{Case 2 part 1:} the left conjunct of case 2, and the tricky part of the proof.

We show this for all $t$ by fixing some $t$ and assuming that $t\ \EL$.
We must show $s_1s_2t\ \EL$.

We will note (without further discussion) that juxtaposition is associative:
\[ (s_1s_2)t = s_1s_2t = s_1(s_2t) \]

We have $IH_2 \equiv P(s_2) \equiv (\forall ~t. ~ t\ \EL ~ \longrightarrow ~ s_2t\ \EL) \wedge s_2\ \EL$. We call its left conjunct $IH_{2a}$ and its right conjunct $IH_{2b}$.

We show our goal by:

\[
    \inferrule{ \inferrule{ }{s_1\ \N}{IH_1}
       \quad \inferrule{ \inferrule{ }{t\ \EL}{\mbox{assumption}} }{s_2t\ \EL}{IH_{2a}}
    }{s_1(s_2t)\ \EL}{L_J}
\]

\proofcase{Case 2 part 2:} the right conjunct of case 2, $s_1s_2\ \EL$.

This is shown simply by:

\[
        \inferrule{ \inferrule{ }{s_1\ \N}{IH_1} \quad \inferrule{ }{s_2\ \EL}{IH_{2b}} }{s_1s_2\ \EL}{L_J}\quad\quad\quad
\]

\proofcase{Case 3:} The inductive case associated with $N_N$.

We assume the inductive hypothesis $IH \equiv P(s)$ and must show $Q(~(s)~) \equiv (s)\ \N$.

The right conjunct of $P(s)$ is $s\ \EL$, which we call $IH_b$. We show our goal simply by:

\[
        \inferrule{ \inferrule{ }{s\ \EL}{IH_b} }{\texttt{(}s\texttt{)}\ \N }{N_N}\quad\quad\quad
\]



\end{document}
