\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{amstext}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\newcommand{\from}{\leftarrow}
\newcommand{\isaname}[1]{\textit{#1}}

\begin{document}

\title{Minsky Machines%
\thanks{This work was supported by FWF (Austrian Science Fund) project P30301.}}
\author{Bertram Felgenhauer}
\maketitle

\begin{abstract}
We formalize undecidablity results for Minsky machines. To this end, we also formalize recursive
inseparability.

We start by proving that Minsky machines can compute arbitrary primitive recursive and recursive
functions. We then show that there is a deterministic Minsky machine with one argument (modeled by
assigning the argument to register $0$ in the initial configuration) and final states $0$ and $1$
such that the set of inputs that are accepted in state $0$ is recursively inseparable from the set
of inputs that are accepted in state $1$.

As a corollary, the set of Minsky configurations that reach state $0$ but not state $1$ is
recursively inseparable from the set of Minsky configurations that reach state $1$ but not
state $0$. In particular both these sets are undecidable.

We do \emph{not} prove that recursive functions can simulate Minsky machines.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
