\documentclass[12pt]{article}
\usepackage{blindtext}
\usepackage{enumerate}
\usepackage{hyperref, bookmark}
\usepackage{amsmath, amsfonts, amssymb, amsthm}
\usepackage{xcolor}

\title{Ideas on Strong Separation}
\author{Anonymous}

\input{macros}
\begin{document}

\maketitle

\newcommand{\Prgm}[2]{[#1\Comma #2]}

\subparagraph{Syntax}
\[\begin{array}{lll}
  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \Prgm{\tm}{\vec\tm} \\
  n & \ddef & \Lam\var \Prgm{n}{\vec n} \mid \var\,\vec n \\
  \\
  C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
  P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\
\end{array}\]

\subparagraph{Reduction}
\[\begin{array}{lll}
  P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\in \Prgm\tm{\vec\tm}} &
   P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\
   P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\Prgm\tm{\vec\tm}} &
    P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\
\end{array}\]

\subparagraph{Properties of the calculus:}
\begin{itemize}
  \item Every term is normalizing iff it is strongly normalizing.
  \item Ogni strategia e' perpetua!
\end{itemize}

\clearpage
\section*{Syntactic Condition}

\begin{definition}[Separable]
  Let $t$, $s$ normal terms.

  They are (semi?) separable iff
  there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$
  S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,
  $t'' <> s''$.
\end{definition}

An occurrence of a bound variable is usable if its head is not stuck.

A head is stuck

\begin{verbatim}
  Ctx[] is stuck (unappicable) if:
   - it is an application and the head variable is stuck
   - it is a garbage
   -

\end{verbatim}

\end{document}
