\documentclass[a4paper]{llncs}
\usepackage{amsmath}
\usepackage{amssymb}

\newcommand{\bimbo}{ Bimb\'{o} }

\newcommand{\limp}{\to}
\newcommand{\verum}{\ensuremath{\mathbf{t}}}

\newcommand{\rarrow}{\ensuremath{R_{\limp}}}
\newcommand{\rarrowt}{\ensuremath{R_{\limp}^{\verum}}}
\newcommand{\tarrow}{\ensuremath{T_{\limp}}}
\newcommand{\tarrowt}{\ensuremath{T_{\limp}^{\verum}}}

\newcommand{\lrarrow}{\ensuremath{LR_{\limp}}}
\newcommand{\lrarrowc}{\ensuremath{\myb{LR_{\limp}}}}
\newcommand{\lrarrowt}{\ensuremath{LR_{\limp}^{\verum}}}
\newcommand{\lrarrowtc}{\ensuremath{\myb{LR_{\limp}^{\verum}}}}
\newcommand{\lrarrowstr}{\ensuremath{LR_{\limp\semic}}}

\newcommand{\ltarrow}{\ensuremath{LT_{\limp\semic}}}
\newcommand{\ltarrowt}{\ensuremath{LT_{\limp\semic}^{\verum}}}
\newcommand{\ltarrowc}{\ensuremath{\myb{LT_{\limp\semic}^{\verum}}}}

\newcommand{\tcirc}{\ensuremath{\bigcirc\!\!\!\!\verum}}
\newcommand{\ltarrowtcirc}{\ensuremath{LT_{\limp\semic}^{\tcirc\;}}}

\newcommand{\str}{\ensuremath{Str}}
\newcommand{\astr}[2]{#1\{#2\}}

\newcommand{\seq}{\ensuremath{\vdash}}
\newcommand{\myb}[1]{\ensuremath{[#1]}}
\newcommand{\semic}{\ensuremath{\; ; \;}}
\newcommand{\smsc}{\ensuremath{;}}
\newcommand{\tick}{\checkmark}

\newcommand{\strttleft}{(T\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strbleft}{(B\ensuremath{\seq\smsc})}
\newcommand{\strbpleft}{(B\ensuremath{'\seq\smsc})}
\newcommand{\strwleft}{(W\ensuremath{\seq\smsc})}

\newcommand{\strktleft}{(K\ensuremath{_{\verum}\seq\smsc})}


\title{Results from their second paper}

\begin{document}

\maketitle

\begin{description}
\item[Page 3:] We proved cut theorems and other important properties
  about these calculi -- including that all agree on the pure
  implicational formulas.
\item[Page 4:] \ltarrowtcirc is equivalent to \rarrowt whereas
  \ltarrowt is equivalent to \tarrowt. The difference between the two
  calculi is that in \ltarrowtcirc, $\verum$ is left identity
  only, and in \ltarrowtcirc, it is full identity because of the two new
  rules $\strktleft$ and $\strttleft$, which are special versions of thinning and
  permutation.
\item[Page 4:] We define an algorithm (called $\pi$), which turns proofs in
  \ltarrowtcirc into proofs in \lrarrowt.
\item[Page 4:] Every theorem of \tarrowt{} has an irredundant proof in
  \lrarrowtc , and it is straightforward to convert those  proofs into
  proofs in \lrarrowt{} that do not contain the ($\seq\verum$) axiom.
\item[Page 4:] We define an algorithm (called $\tau$), which turns
  proofs in \lrarrowt{} into proofs in \ltarrowtcirc{}, by restoring
  the distinctions inherent to \ltarrowtcirc.  
\item[Page 4:] In section 1, we prove that the addition of the
  constant \verum{} does not prevent the decidability of \rarrow{} to be
  extended to \rarrowt.
\item[Page 4:] In section 2, we consider the relationship of the
  calculi \ltarrowtcirc and \lrarrowt, especially, from the point of
  view of transforming proofs in the former into proofs in the latter.
\item[Page 4:] Section 3 describes the transformations 
from \lrarrowtc{} to \lrarrowt, and
  further, to \ltarrowtcirc.
\item[Page 4:] Section 4 completes the proof of the decidability of
  \ltarrow. There we show that proofs that do not belong to
  \ltarrowt{} can be unequivocally distinguished from those that do.
\item[Page 4:]It is well-known that \rarrowt is conservative over
  \rarrow, which also follows from the cut theorem for \lrarrowtc.
\item[Page 4:] A consecution calculus for \tarrow has to include
  \verum. Footnote 7 then says: There is a consecution calculus for
  \tarrow{} without \verum{} in \bimbo 2007b Section 3.2. However, the
  absence of \verum{} makes the calculus intricate and difficult to
  use. There is a so-called merge calculus for \tarrow{} in Anderson and
  Belnap (1975), which is more similar to a sequent calculus than to a
  consecution calculus. We are not aware of the existence of a sequent
  calculus (of the usual sort) for \tarrow.
\item[Page 4:] Therefore, we first prove that the conservative
  extension of \lrarrowc{} with \verum{} inherits decidability from
  \lrarrowtc (Raj thinks this should be just \lrarrowc ).
\item[Curry's Lemma:] Curry’s Lemma states that if a sequent
  $\alpha'\seq A$ is obtainable by contractions from a sequent
  $\alpha \seq A$ and the latter has a proof in \lrarrowc, then
  $\alpha' \seq A$ has a proof in \lrarrowc{} of length less than or equal
  to the length of the proof of $\alpha \seq A$.

  \begin{quote}
    So this is just height-preserving contraction admissibility for \lrarrowc?
  \end{quote}
\item[Page 5:] A proof tree is redundant if it contains a branch with
  a sequent $\alpha' \seq A$ below another sequent $\alpha \seq A$
  from which it can be obtained by contractions (including the
  degenerate case of the null contraction, i.e., where a sequent is
  simply repeated).
\item[Page 5:] This opens the door to Kripke's distinctive
  contribution, which shows that every branch in such an irredundant
  proof search tree is finite. First, two sequents $\alpha \seq A$ and
  $\alpha' \seq A$ are said to be cognate, when exactly the same
  formulas -- not counting multiplicity -- occur in them. This
  partitions sequents into cognation classes. Kripke's Lemma says that
  if a sequence of distinct cognate sequents $\Gamma_0, \Gamma_1,
  \cdots $, is irredundant in the sense that for no $\Gamma_i,
  \Gamma_j$ (where $i < j$), $\Gamma_i$ is obtainable from $\Gamma_j$
  by contractions, then the sequence is finite.
\item[Page 5:] Lemma 1. If a sequent $\alpha' \seq A$ is obtainable by
  contractions from a sequent $\alpha \seq A$ and the latter has a
  proof in \lrarrowtc, then $\alpha' \seq A$ has a proof of length
  less than or equal to the length of the proof of $\alpha\seq A$. The
  proof is by induction on the length of the proof of $\alpha\seq A$.

  \begin{quote}
    Raj: So \lrarrowtc{} has contraction admissibility?
  \end{quote}

\item[Page 6:] We proved in \bimbo and Dunn (2012b) (see lemma 2.5)
  that \rarrow{} and \lrarrowc{} have the same set of theorems.
\item[Page 6:] \rarrowt{} is decidable.
\item[Page 6:] We proved in \bimbo and Dunn (2012b, Section 4) that
  the single cut rule is admissible in \ltarrowtcirc{} and that $A$ is
  a theorem of \rarrowt{} iff $\verum\seq A$ is provable in
  \ltarrowtcirc. The cut theorem implies that $\verum\seq A$ has a
  cut-free proof in \ltarrowtcirc provided $A$ is a theorem of \rarrowt.
\item[Page 7:] Definition ($\pi$) transformation. Let $\delta$ be a
  proof in \ltarrowtcirc{}. The transformation $\pi$ of $\delta$ is the
  following consecutive applications of steps (1)-(4):
  \begin{enumerate}
  \item replace every $\semic$ by a comma;
  \item Omit all the parentheses from complex structures
  \item Omit the lower sequent, if the corresponding lower consecution
    was the  result of an application of the \strbleft, \strbpleft, or
    \strttleft{} rules.
  \item Insert finitely many sequents between 
    $\Gamma, A_1, A_1, A_2, A_2, \cdots , A_n, A_n \seq B$ 
    and 
    $\Gamma, A_1, A_2, \cdots , A_n \seq B$ 
    if the corresponding lower consecution resulted by an application
    of \strwleft{} to two occurrences of a complex structure comprising
    $n$ atomic structures that we denote by $A_1, \cdots , A_n$. The
    inserted $n-1$ sequents are consecutive contractions of
    $A_1, \cdots , A_n$
    starting from 
    $\Gamma, A_1, A_1, A_2, A_2, \cdots , A_n, A_n \seq B$.
  \end{enumerate}
  \item[Page 7:] The transformation in effect ``blurs'' the proof $\delta$ so
    that (1) semi-colons are seen as commas, (2) parentheses are not
    seen (unless they are in a formula), (3) identical sequents just
    above each other are squashed into one, and (4) contractions of
    complex structures are emulated by consecutive contractions on
    their atomic structures.  For our purposes, it is even more
    important that certain features of the proofs are not destroyed.
  \item[Page 7:] Footnote 11 says This list may contain multiple
    occurrences of a formula; however, for the purposes of describing
    this step it is easier to work with a listing of atomic structures
    whether they are identical formulas or not.
  \item[Page 7:] Notice that if $n > 1$ in step (4), then different
    orderings of contractions (of different formulas) result in
    distinct proofs in \lrarrowt.  We give an example of the
    transformation.
  \item[Page 8:] Let $\pi(U \seq A)$ be the result of apply steps
    (1)-(2) from this definition. It is obvious that $\pi(U \seq A)$
    is a traditional sequent.
  \item[Page 8:] Lemma 4 (Simplification). If $\delta$ is a proof in
    the sense of \ltarrowtcirc, then $\pi(\delta)$ obtained by the
    transformation is a proof in \lrarrowt.
  \item[Page 9:] Lemma 5: If $A$ is a theorem of \tarrowt, then
    $\verum\seq A$ is provable in \lrarrowtc. However, it may be
    useful to emphasise that $A$ has an irrerundant proof in
    \lrarrowtc.
  \item[Page 10:] Lemma 6. If $\delta$ is a proof in \ltarrowt, then
    $\pi(\delta)$ contains the applications of the connective rules
    and of the contraction rule in the original order in $\delta$.
  \item[Page 10:] If A is a theorem of \rarrow, then it is provable in \ltarrowt
    (without the cut rule).
  \item Every theorem of \tarrow is of the form $A_1 \limp A_2 \limp
    \cdots \limp (A_n \limp p)$ where $n \in \mathbb{N}^+$ and $p$ is a
    propositional variable.
  \item We will assume that a given formula $A$ is tested for
    provability using \lrarrowtc. This can mean -- equivalently -- searching
    for a proof of either of the sequents $\verum \seq A$ or $\seq A$.
  \item[Page 12:] Lemma 7. If $\delta$ is a proof of $\verum \seq A$ in
    \lrarrow, then there is a proof $\delta'$ of the same end sequent that
    does not contain occurrences of the axiom $\seq \verum$.
  \item[Page 13] Lemma 8. If $\astr{U}{X \semic Y} \seq A$ is provable in
    \ltarrowtcirc, then $\astr{U}{\verum \semic Y \semic X} \seq  A$ and 
    $\astr{U}{\verum \semic (Y \semic X)} \seq A$ are provable
  \item[Page 13] Lemma 9. If $\astr{U}{X \semic Y \semic Z} \seq A$ is provable
    in \ltarrowtcirc, then $\astr{U}{V} \seq A$ is provable too, where
    $V$ is any permutation and grouping of the three structures $X$
    and $Y$ and $Z$ with a $\verum$ on the left and associated with the
    leftmost of those three structures.
  \item[Page 14] Lemma 10. If $\astr{U}{ X \semic Y \semic Z} \seq A$ is
    provable in \ltarrowtcirc, then $\astr{U}{V} \seq A$ is provable
    too, where $V$ is any permutation and grouping of the three
    structures $X$ and $Y$ and $Z$ associated together with a $\verum$ as
    the leftmost structure.
  \item[Page 15] If there are $n > 1$ consecutive applications of the \strwleft
    rule in $\delta$ at this point, then we consider them
    together. First, we divide n into all the possible ordered sums
    (including $n$ itself). (For example, if $n = 3$ then we get $1 + 1 +
    1$, $1 + 2$, $2 + 1$ and $3$.)  It is trivial that there are finitely
    many possibilities for each n. The total number of ordered sums is
    $2^{n−1}$.
  \item[Page 18] Lemma 11 (Distinction). If $A$ is a theorem of \tarrow{}
    with $\seq\verum$-free proofs $\delta_1$, $\delta_2$, $\cdots$,
    $\delta_n$ in \lrarrowt obtained from the irredundant proofs of
    $\verum \seq A$ in \lrarrowtc, then $\exists i$ such that $\tau
    (\delta_i)$ is a proof of $\verum\seq A$ in $\ltarrow$.
\end{description}
\end{document}