diff --git a/thys/Call_Arity/document/root.tex b/thys/Call_Arity/document/root.tex
--- a/thys/Call_Arity/document/root.tex
+++ b/thys/Call_Arity/document/root.tex
@@ -1,243 +1,240 @@
 \documentclass[11pt,a4paper,parskip=half]{scrartcl}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
 \usepackage[only,bigsqcap]{stmaryrd}
 
 \newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}
 
 \usepackage{amsmath}
 \usepackage{mathtools}
 \usepackage{graphicx}
 \usepackage{tikz}
 \usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
 \usepackage{mathpartir}
 \usepackage{calc}
 \usepackage{booktabs}
 \usepackage{longtable}
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theorys in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % Isabelle does not like *} in a text {* ... *} block
 % Concrete implemenation thanks to http://www.mrunix.de/forums/showpost.php?p=235085&postcount=5
 \newenvironment{alignstar}{\csname align*\endcsname}{\csname endalign*\endcsname}
 \newenvironment{alignatstar}{\csname alignat*\endcsname}{\csname endalignat*\endcsname}
 
 % quench koma warnings
 \def\bf{\normalfont\bfseries}
 \def\it{\normalfont\itshape}
 \def\rm{\normalfont}
 \def\sc{\normalfont\scshape}
 
-% Instead of using utf8x
-\DeclareUnicodeCharacter{B2}{\ensuremath{^2}}
-
 % from http://tex.stackexchange.com/a/12931
 \begingroup
   \catcode`\_=\active
   \gdef_#1{\ensuremath{\sb{\mathrm{#1}}}}
 \endgroup
 \mathcode`\_=\string"8000
 \catcode`\_=12
 
 \begin{document}
 
 \title{The Safety of Call Arity}
 \author{Joachim Breitner\\
 Programming Paradigms Group\\
 Karlsruhe Institute for Technology\\
 \url{breitner@kit.edu}}
 \maketitle
 
 
 \begin{abstract}
 We formalize the Call Arity analysis \cite{tfp}, as implemented in GHC, and prove both functional correctness and, more interestingly, safety (i.e.\ the transformation does not increase allocation). A highlevel overview of the work can be found in \cite{call-arity-haskell15}.
 
 We use syntax and the denotational semantics from an earlier work \cite{breitner2013}, where we formalized Launchbury's natural semantics for lazy evaluation \cite{launchbury}. 
 The functional correctness of Call Arity is proved with regard to that denotational semantics.
 The operational properties are shown with regard to a small-step semantics akin to Sestoft's mark 1 machine \cite{sestoft}, which we prove to be equivalent to Launchbury's semantics.
 
 We use Christian Urban's Nominal2 package \cite{nominal} to define our terms and make use of Brian Huffman's HOLCF package for the domain-theoretical aspects of the development \cite{holcf}.
 
 \end{abstract}
 
 \section*{Artifact correspondence table}
 \label{sec:table}
 
 The following table connects the definitions and theorems from \cite{call-arity-haskell15} with their corresponding Isabelle concept in this development.
 
 \newcommand{\seetheory}[1]{\hyperref[sec_#1]{#1}}
 
 \begin{center}
 \begin{longtable}[h]{lll}
 \textsf{Concept} & \textsf{corresponds to} & \textsf{in theory} \\
 \midrule
 Syntax                                                        & \isacommand{nominal-datatype} \isa{expr}                  & Terms in \cite{breitner2013} \\
 Stack                                                         & \isacommand{type-synonym} \isa{stack}                     & \seetheory{SestoftConf} \\
 Configuration                                                 & \isacommand{type-synonym} \isa{conf}                      & \seetheory{SestoftConf} \\
 Semantics ($\Rightarrow$)                                     & \isacommand{inductive} \isa{step}                         & \seetheory{Sestoft} \\
 Arity                                                         & \isacommand{typedef} \isa{Arity}                          & \seetheory{Arity} \\
 Eta-expansion                                                 & \isacommand{lift-definition} \isa{Aeta-expand}            & \seetheory{ArityEtaExpansion} \\
 Lemma 1                                                       & \isacommand{theorem} \isa{Aeta-expand-safe}            & \seetheory{ArityEtaExpansionSafe} \\
 $\mathcal A_\alpha(\Gamma, e)$                                & \isacommand{locale} \isa{ArityAnalysisHeap}               & \seetheory{ArityAnalysisSig} \\
 $\mathsf T_\alpha(e)$                                         & \isacommand{sublocale} \isa{AbstractTransformBound}       & \seetheory{ArityTransform} \\
 $\mathcal A_\alpha(e)$                                        & \isacommand{locale} \isa{ArityAnalysis}                   & \seetheory{ArityAnalysisSig} \\
 Definition 2                                                  & \isacommand{locale} \isa{ArityAnalysisLetSafe}         & \seetheory{ArityAnalysisSpec} \\
 Definition 3                                                  & \isacommand{locale} \isa{ArityAnalysisLetSafeNoCard}   & \seetheory{ArityAnalysisSpec} \\
 Definition 4                                                  & \isacommand{inductive} \isa{a-consistent}                 & \seetheory{ArityConsistent} \\
 Definition 5                                                  & \isacommand{inductive} \isa{consistent}                   & \seetheory{ArityTransformSafe} \\
 Lemma 2                                                       & \isacommand{lemma} \isa{arity-transform-safe}             & \seetheory{ArityTransformSafe} \\
 % Concrete arity analysis                                     & \isacommand{definition} \isa{Real-Aexp}                   & \seetheory{ArityAnalysisImpl} \\
 $\operatorname{Card}$                                         & \isacommand{type-synonym} \isa{two}                       & \seetheory{Cardinality-Domain} \\
 $\mathcal C_\alpha(\Gamma, e)$                                & \isacommand{locale} \isa{CardinalityHeap}                 & \seetheory{CardinalityAnalysisSig} \\
 $\mathcal C_{(\bar\alpha,\alpha,\dot\alpha)}((\Gamma, e, S))$ & \isacommand{locale} \isa{CardinalityPrognosis}            & \seetheory{CardinalityAnalysisSig} \\
 Definition 6                                                  & \isacommand{locale} \isa{CardinalityPrognosisSafe}     & \seetheory{CardinalityAnalysisSpec} \\
 Definition 7 ($\Rightarrow_\#$)                               & \isacommand{inductive} \isa{gc-step}                      & \seetheory{SestoftGC} \\
 Definition 8                                                  & \isacommand{inductive} \isa{consistent}                   & \seetheory{CardArityTransformSafe} \\
 Lemma 3                                                       & \isacommand{lemma} \isa{card-arity-transform-safe}        & \seetheory{CardArityTransformSafe} \\
 Trace trees                                                   & \isacommand{typedef} \isa{'a ttree}                       & \seetheory{TTree} \\
 Function $s$                                                  & \isacommand{lift-definition} \isa{substitute}             & \seetheory{TTree} \\
 $\mathcal T_\alpha(e)$                                        & \isacommand{locale} \isa{TTreeAnalysis}                   & \seetheory{TTreeAnalysisSig} \\
 $\mathcal T_\alpha(\Gamma,e)$                                 & \isacommand{locale} \isa{TTreeAnalysisCardinalityHeap}    & \seetheory{TTreeAnalysisSpec} \\
 Definition 9                                                  & \isacommand{locale} \isa{TTreeAnalysisCardinalityHeap}    & \seetheory{TTreeAnalysisSpec} \\
 Lemma 4                                                       & \isacommand{sublocale} \isa{CardinalityPrognosisSafe}  & \seetheory{TTreeImplCardinalitySafe} \\
 Co-Call graphs                                                & \isacommand{typedef} \isa{CoCalls}                        & \seetheory{CoCallGraph} \\
 Function $g$                                                  & \isacommand{lift-definition} \isa{ccApprox}               & \seetheory{CoCallGraph-TTree} \\
 Function $t$                                                  & \isacommand{lift-definition} \isa{ccTTree}                & \seetheory{CoCallGraph-TTree} \\
 $\mathcal G_\alpha(e)$                                        & \isacommand{locale} \isa{CoCallAnalysis}                  & \seetheory{CoCallAnalysisSig} \\
 $\mathcal G_\alpha(\Gamma, e)$                                & \isacommand{locale} \isa{CoCallAnalysisHeap}              & \seetheory{CoCallAnalysisSig} \\
 Definition 10                                                 & \isacommand{locale} \isa{CoCallAritySafe}              & \seetheory{CoCallAnalysisSpec} \\
 Lemma 5                                                       & \isacommand{sublocale} \isa{TTreeAnalysisCardinalityHeap} & \seetheory{CoCallImplTTreeSafe} \\
 Call Arity & \isacommand{nominal-function} \isa{cCCexp}                & \seetheory{CoCallAnalysisImpl} \\
 Theorem 1                                                     & \isacommand{lemma} \isa{end2end-closed}                   & \seetheory{CallArityEnd2EndSafe} \\
 \end{longtable}
 \end{center}
 
 \bibliographystyle{amsalpha}
 \bibliography{\jobname}
 
 \tableofcontents
 \newcommand{\theory}[1]{\subsection{#1}\label{sec_#1}\input{#1.tex}}
 
 %\let\OldInput\input
 %\renewcommand{\input}[1]{{
 %        \subsection{#1}
 %        \OldInput{#1}
 %}}
 
 %\OldInput{session.tex}
 
 
 \section{Various Utilities}
 
 \theory{ConstOn}
 \theory{Set-Cpo}
 \theory{Env-Set-Cpo}
 \theory{AList-Utils-HOLCF}
 \theory{List-Interleavings}
 
 
 
 \section{Small-step Semantics}
 \theory{SestoftConf}
 \theory{Sestoft}
 \theory{SestoftGC}
 \theory{BalancedTraces}
 \theory{SestoftCorrect}
 
 \section{Arity}
 \theory{Arity}
 \theory{AEnv}
 \theory{Arity-Nominal}
 \theory{ArityStack}
 
 \section{Eta-Expansion}
 
 \theory{EtaExpansion}
 \theory{EtaExpansionSafe}
 \theory{TransformTools}
 \theory{ArityEtaExpansion}
 \theory{ArityEtaExpansionSafe}
 
 \section{Arity Analysis}
 
 \theory{ArityAnalysisSig}
 \theory{ArityAnalysisAbinds}
 \theory{ArityAnalysisSpec}
 \theory{TrivialArityAnal}
 \theory{ArityAnalysisStack}
 
 \theory{ArityAnalysisFix}
 \theory{ArityAnalysisFixProps}
 
 \section{Arity Transformation}
 
 \theory{AbstractTransform}
 \theory{ArityTransform}
 
 
 \section{Arity Analysis Safety (without Cardinality)}
 \theory{ArityConsistent}
 \theory{ArityTransformSafe}
 
 \section{Cardinality Analysis}
 
 \theory{Cardinality-Domain}
 \theory{CardinalityAnalysisSig}
 \theory{CardinalityAnalysisSpec}
 
 \theory{NoCardinalityAnalysis}
 
 \theory{CardArityTransformSafe}
 
 \section{Trace Trees}
 \theory{TTree}
 \theory{TTree-HOLCF}
 
 \section{Trace Tree Cardinality Analysis}
 \theory{AnalBinds}
 \theory{TTreeAnalysisSig}
 \theory{Cardinality-Domain-Lists}
 \theory{TTreeAnalysisSpec}
 \theory{TTreeImplCardinality}
 \theory{TTreeImplCardinalitySafe}
 
 
 \section{Co-Call Graphs}
 \theory{CoCallGraph}
 \theory{CoCallGraph-Nominal}
 
 \section{Co-Call Cardinality Analysis}
 
 \theory{CoCallAnalysisSig}
 \theory{CoCallAnalysisBinds}
 \theory{CoCallAritySig}
 \theory{CoCallAnalysisSpec}
 \theory{CoCallFix}
 
 \theory{CoCallGraph-TTree}
 \theory{CoCallImplTTree}
 \theory{CoCallImplTTreeSafe}
 
 \section{CoCall Cardinality Implementation}
 \theory{CoCallAnalysisImpl}
 \theory{CoCallImplSafe}
 
 \section{End-to-end Saftey Results and Example}
 \theory{CallArityEnd2End}
 \theory{CallArityEnd2EndSafe}
 
 \section{Functional Correctness of the Arity Analysis}
 \theory{ArityAnalysisCorrDenotational}
 
 %%% Local Variables:
 %%% mode: l
 %%% TeX-master: "root"
 %%% End:
 
 \end{document}
diff --git a/thys/LOFT/document/root.tex b/thys/LOFT/document/root.tex
--- a/thys/LOFT/document/root.tex
+++ b/thys/LOFT/document/root.tex
@@ -1,125 +1,122 @@
 \documentclass[a4paper]{article}
 \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>
 
 \usepackage[utf8]{inputenc}
 \usepackage{makeidx}
 \usepackage{graphicx}
 \usepackage{tabularx}
 \usepackage{amssymb}
 \usepackage{amsmath}
 \usepackage{color}
 \usepackage{booktabs}
 \newcommand{\todo}[1]{\textcolor{red}{TODO: #1}}
 \usepackage{pifont}
 \usepackage{tikz}
 \usetikzlibrary{calc}
 \usepackage{moeptikz}
-\DeclareUnicodeCharacter{2713}{\ding{52}}
-\DeclareUnicodeCharacter{2717}{\ding{56}}
-\DeclareUnicodeCharacter{00D7}{\ensuremath{\times}}%               \<times>
 \usepackage{flushend}
 \usepackage{stmaryrd}
 \usepackage{mathtools}
 \hyphenation{swit-ches}
 \usepackage{alphabeta}
 \usepackage{url}
 \usepackage{tikz}
 \usetikzlibrary{calc,positioning}
 \widowpenalty100000
 \clubpenalty100000
 \usepackage{pbox}
 \usepackage{subcaption}
 \usepackage{framed}
 \usepackage{listings}
 \lstset{breaklines=true,numbers=left,numberstyle=\tiny\color{gray},basicstyle=\footnotesize\ttfamily}
 \usepackage{pgfplots}
 \columnsep 2pc          %    Space between columns
 \textwidth 42pc         % Width of text line.
 \oddsidemargin 4.5pc
 \evensidemargin 4.5pc
 \advance\oddsidemargin by -1.11in  % Correct for LaTeX gratuitousness
 \advance\evensidemargin by -1.11in % Correct for LaTeX gratuitousness
 \marginparwidth 0pt             % Margin pars are not allowed.
 \marginparsep 11pt              % Horizontal space between outer margin and
 \emergencystretch=10cm
 
 
 % 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}
 
 \usepackage[english]{babel}
 % for \frqq (whatever that actually is)
 
 \begin{document}
 \title{LOFT — Verified Migration of Linux Firewalls to SDN}
 \author{Julius Michaelis and Cornelius Diekmann}
 \maketitle
 
 \begin{abstract}
 	We present LOFT — \emph{L}inux firewall \emph{O}pen\emph{F}low \emph{T}ranslator, a system that transforms the main routing table and \texttt{FORWARD} chain of iptables of a Linux-based firewall into a set of static OpenFlow rules.
 	Our implementation is verified against a model of a simplified Linux-based router and we can directly show how much of the original functionality is preserved.
 \end{abstract}
 \vspace{1em}
 
 Please note that this document is organized in two distinct parts.
 The first part contains the necessary definitions, helper lemmas and proofs in all their technicality as made in the theory code.
 The second part reiterates the most important definitions and proofs in a manner that is more suitable for human readers and enriches them with detailed explanations in natural language.
 Any interested reader should start from there.
 
 Many of the considerations that have led to the definitions made here have been explained in \cite{michaelis2016middlebox}.
 
 \tableofcontents
 
 \newpage
 
 \part{Code}
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 \input{session}
 
 \input{chap3}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
 
diff --git a/thys/Propositional_Proof_Systems/document/fig_sema.tex b/thys/Propositional_Proof_Systems/document/fig_sema.tex
--- a/thys/Propositional_Proof_Systems/document/fig_sema.tex
+++ b/thys/Propositional_Proof_Systems/document/fig_sema.tex
@@ -1,399 +1,399 @@
 
 \begin{tikzpicture}[>=latex,line join=bevel,scale=0.15, every node/.style={scale=0.3}]
   \pgfsetlinewidth{1bp}
 %%
 \pgfsetcolor{black}
   % Edge: Compactness -> Sema
   \draw [->,-stealth,very thin] (1048.3bp,355.57bp) .. controls (1066.7bp,364.9bp) and (1090.7bp,375.86bp)  .. (1113.2bp,382.36bp) .. controls (1226.3bp,414.96bp) and (1362.8bp,428.13bp)  .. (1455.5bp,433.99bp);
   % Edge: ND -> Formulas
   \draw [->,-stealth,very thin] (926.55bp,443.99bp) .. controls (1109.8bp,457.9bp) and (1509.2bp,488.24bp)  .. (1703.2bp,502.98bp);
   % Edge: Resolution_Compl_Consistency -> Consistency
   \draw [->,-stealth,very thin] (2283.9bp,137.24bp) .. controls (2089.0bp,151.32bp) and (1706.3bp,180.75bp)  .. (1681.2bp,196.45bp) .. controls (1653.7bp,213.61bp) and (1665.1bp,234.82bp)  .. (1643.2bp,258.68bp) .. controls (1627.6bp,275.6bp) and (1608.0bp,291.26bp)  .. (1581.4bp,309.88bp);
   % Edge: Resolution_Compl_SC_Small -> LSC_Resolution
   \draw [->,-stealth,very thin] (1947.7bp,61.922bp) .. controls (1929.4bp,75.847bp) and (1908.1bp,92.063bp)  .. (1883.0bp,111.22bp);
   % Edge: SC_Depth_Limit -> SC_Depth
   \draw [->,-stealth,very thin] (109.03bp,258.77bp) .. controls (109.35bp,270.58bp) and (109.72bp,284.23bp)  .. (110.34bp,307.16bp);
   % Edge: Resolution_Compl_Consistency -> CNF_Formulas_Sema
   \draw [->,-stealth,very thin] (2475.1bp,152.19bp) .. controls (2519.7bp,165.15bp) and (2576.6bp,181.67bp)  .. (2627.2bp,196.45bp) .. controls (2635.2bp,198.79bp) and (2643.5bp,201.23bp)  .. (2661.6bp,206.53bp);
   % Edge: SCND -> ND
   \draw [->,-stealth,very thin] (694.38bp,355.15bp) .. controls (706.76bp,363.51bp) and (722.14bp,373.69bp)  .. (736.19bp,382.36bp) .. controls (753.65bp,393.14bp) and (773.29bp,404.5bp)  .. (799.21bp,419.13bp);
   % Edge: ND_Compl_SC -> SC_Sema
   \draw [->,-stealth,very thin] (565.53bp,251.64bp) .. controls (512.13bp,271.52bp) and (437.2bp,299.42bp)  .. (377.36bp,321.7bp);
   % Edge: Resolution_Compl_SC_Small -> Resolution
   \draw [->,-stealth,very thin] (2256.7bp,35.24bp) .. controls (2503.6bp,41.586bp) and (2838.2bp,57.647bp)  .. (2885.2bp,98.225bp) .. controls (2913.6bp,122.74bp) and (2917.6bp,168.47bp)  .. (2916.2bp,208.73bp);
   % Edge: LSC_Resolution -> Resolution
   \draw [->,-stealth,very thin] (1955.3bp,136.93bp) .. controls (2038.8bp,143.44bp) and (2163.0bp,152.93bp)  .. (2271.2bp,160.45bp) .. controls (2523.5bp,177.97bp) and (2592.8bp,139.21bp)  .. (2839.2bp,196.45bp) .. controls (2850.2bp,199.02bp) and (2861.7bp,203.04bp)  .. (2881.7bp,211.36bp);
   % Edge: MiniFormulas_Sema -> Sema
   \draw [->,-stealth,very thin] (2027.7bp,369.31bp) .. controls (2013.8bp,374.39bp) and (1999.2bp,379.06bp)  .. (1985.2bp,382.36bp) .. controls (1815.3bp,422.3bp) and (1766.3bp,389.24bp)  .. (1594.2bp,418.36bp) .. controls (1588.7bp,419.28bp) and (1583.1bp,420.4bp)  .. (1567.3bp,423.9bp);
   % Edge: CNF_Formulas -> CNF
   \draw [->,-stealth,very thin] (2447.7bp,353.76bp) .. controls (2518.8bp,373.24bp) and (2640.4bp,406.61bp)  .. (2715.6bp,427.26bp);
   % Edge: Substitution_Sema -> Sema
   \draw [->,-stealth,very thin] (1781.5bp,354.74bp) .. controls (1724.1bp,372.77bp) and (1631.7bp,401.74bp)  .. (1563.9bp,423.04bp);
   % Edge: Resolution_Compl_SC_Small -> SC_Sema
   \draw [->,-stealth,very thin] (1760.4bp,47.997bp) .. controls (1690.7bp,52.906bp) and (1613.8bp,58.061bp)  .. (1543.2bp,62.225bp) .. controls (1210.0bp,81.864bp) and (1124.4bp,57.444bp)  .. (793.19bp,98.225bp) .. controls (571.88bp,125.47bp) and (442.58bp,24.034bp)  .. (301.19bp,196.45bp) .. controls (274.23bp,229.32bp) and (296.15bp,280.41bp)  .. (319.52bp,320.13bp);
   % Edge: Tseytin -> CNF_Formulas
   \draw [->,-stealth,very thin] (2264.1bp,245.64bp) .. controls (2290.0bp,264.39bp) and (2330.6bp,293.82bp)  .. (2367.5bp,320.63bp);
   % Edge: SC_Sema -> Sema
   \draw [->,-stealth,very thin] (370.85bp,355.86bp) .. controls (394.19bp,365.48bp) and (424.83bp,376.63bp)  .. (453.19bp,382.36bp) .. controls (549.6bp,401.83bp) and (1218.8bp,426.37bp)  .. (1455.5bp,434.56bp);
   % Edge: ND_Compl_SC -> Compactness
   \draw [->,-stealth,very thin] (704.01bp,249.15bp) .. controls (716.38bp,252.51bp) and (729.11bp,255.81bp)  .. (741.19bp,258.68bp) .. controls (822.69bp,278.0bp) and (846.69bp,268.28bp)  .. (926.19bp,294.68bp) .. controls (943.42bp,300.4bp) and (961.59bp,308.66bp)  .. (986.43bp,321.25bp);
   % Edge: SCND -> SC
   \draw [->,-stealth,very thin] (646.44bp,355.18bp) .. controls (623.87bp,371.01bp) and (589.69bp,394.99bp)  .. (555.95bp,418.66bp);
   % Edge: Resolution_Compl_SC_Full -> Resolution
   \draw [->,-stealth,very thin] (1518.9bp,45.42bp) .. controls (1576.5bp,51.519bp) and (1645.7bp,58.153bp)  .. (1708.2bp,62.225bp) .. controls (1771.6bp,66.363bp) and (2798.9bp,63.505bp)  .. (2852.2bp,98.225bp) .. controls (2856.8bp,101.25bp) and (2885.0bp,162.66bp)  .. (2905.9bp,209.06bp);
   % Edge: LSC -> SC_Cut
   \draw [->,-stealth,very thin] (1148.4bp,242.85bp) .. controls (1103.9bp,248.13bp) and (1053.3bp,253.9bp)  .. (1007.2bp,258.68bp) .. controls (829.64bp,277.05bp) and (777.52bp,241.3bp)  .. (607.19bp,294.68bp) .. controls (597.06bp,297.85bp) and (586.81bp,302.49bp)  .. (568.27bp,312.57bp);
   % Edge: LSC -> CNF_Formulas
   \draw [->,-stealth,very thin] (1372.2bp,250.14bp) .. controls (1389.7bp,253.49bp) and (1407.9bp,256.53bp)  .. (1425.2bp,258.68bp) .. controls (1770.0bp,301.65bp) and (1862.0bp,246.61bp)  .. (2206.2bp,294.68bp) .. controls (2247.5bp,300.44bp) and (2293.1bp,311.12bp)  .. (2338.6bp,323.09bp);
   % Edge: SC_Depth -> SC
   \draw [->,-stealth,very thin] (162.18bp,363.74bp) .. controls (177.63bp,370.59bp) and (194.84bp,377.46bp)  .. (211.19bp,382.36bp) .. controls (283.73bp,404.09bp) and (368.32bp,418.01bp)  .. (442.22bp,427.61bp);
   % Edge: MiniFormulas -> Formulas
   \draw [->,-stealth,very thin] (2027.2bp,451.21bp) .. controls (1978.2bp,463.19bp) and (1908.6bp,480.24bp)  .. (1847.3bp,495.26bp);
   % Edge: CNF_To_Formula -> CNF_Formulas
   \draw [->,-stealth,very thin] (2485.5bp,257.01bp) .. controls (2465.2bp,274.72bp) and (2439.7bp,297.02bp)  .. (2412.9bp,320.42bp);
   % Edge: CNF_Formulas -> Formulas
   \draw [->,-stealth,very thin] (2375.9bp,356.84bp) .. controls (2350.9bp,383.56bp) and (2300.4bp,432.47bp)  .. (2246.2bp,455.13bp) .. controls (2183.6bp,481.32bp) and (2002.8bp,496.7bp)  .. (1878.1bp,504.73bp);
   % Edge: SC_Cut -> SC
   \draw [->,-stealth,very thin] (530.19bp,369.87bp) .. controls (530.19bp,382.07bp) and (530.19bp,395.97bp)  .. (530.19bp,418.25bp);
   % Edge: ND_Compl_Truthtable_Compact -> ND_Compl_Truthtable
   \draw [->,-stealth,very thin] (894.7bp,160.42bp) .. controls (892.15bp,168.75bp) and (889.36bp,177.88bp)  .. (883.72bp,196.35bp);
   % Edge: SC -> Formulas
   \draw [->,-stealth,very thin] (617.62bp,446.1bp) .. controls (649.56bp,449.29bp) and (685.98bp,452.67bp)  .. (719.19bp,455.13bp) .. controls (1075.1bp,481.46bp) and (1498.5bp,498.87bp)  .. (1698.6bp,506.32bp);
   % Edge: Sema_Craig -> Substitution_Sema
   \draw [->,-stealth,very thin] (1958.0bp,255.56bp) .. controls (1930.4bp,273.9bp) and (1894.8bp,297.61bp)  .. (1860.1bp,320.61bp);
   % Edge: ND_Compl_Truthtable_Compact -> Compactness
   \draw [->,-stealth,very thin] (962.96bp,154.85bp) .. controls (980.07bp,165.23bp) and (996.91bp,178.98bp)  .. (1007.2bp,196.45bp) .. controls (1027.7bp,231.34bp) and (1026.1bp,279.7bp)  .. (1020.8bp,319.96bp);
   % Edge: SC_Compl_Consistency -> SC_Cut
   \draw [->,-stealth,very thin] (442.35bp,257.3bp) .. controls (457.74bp,271.53bp) and (476.27bp,288.67bp)  .. (500.01bp,310.61bp);
   % Edge: Tseytin -> Formulas
   \draw [->,-stealth,very thin] (2241.5bp,245.96bp) .. controls (2246.0bp,289.56bp) and (2250.4bp,399.67bp)  .. (2190.2bp,455.13bp) .. controls (2168.1bp,475.44bp) and (1997.3bp,492.84bp)  .. (1875.5bp,503.04bp);
   % Edge: CNF_Formulas_Sema -> CNF_Formulas
   \draw [->,-stealth,very thin] (2665.0bp,249.75bp) .. controls (2602.3bp,270.15bp) and (2510.3bp,300.07bp)  .. (2441.2bp,322.56bp);
   % Edge: SC_Compl_Consistency -> SC_Sema
   \draw [->,-stealth,very thin] (388.67bp,258.18bp) .. controls (376.87bp,274.95bp) and (362.39bp,295.56bp)  .. (345.1bp,320.15bp);
   % Edge: Tseytin_Sema -> Sema
   \draw [->,-stealth,very thin] (1245.4bp,147.45bp) .. controls (1192.8bp,158.91bp) and (1136.9bp,175.52bp)  .. (1121.2bp,196.45bp) .. controls (1104.6bp,218.59bp) and (1106.1bp,235.48bp)  .. (1121.2bp,258.68bp) .. controls (1194.0bp,370.88bp) and (1355.8bp,413.0bp)  .. (1459.4bp,429.91bp);
   % Edge: Resolution -> CNF
   \draw [->,-stealth,very thin] (2878.4bp,243.11bp) .. controls (2836.6bp,261.4bp) and (2772.7bp,289.89bp)  .. (2769.2bp,294.68bp) .. controls (2744.9bp,327.65bp) and (2744.0bp,376.95bp)  .. (2747.4bp,418.1bp);
   % Edge: Resolution_Compl_Consistency -> CNF_Formulas
   \draw [->,-stealth,very thin] (2395.6bp,160.65bp) .. controls (2394.8bp,201.08bp) and (2393.5bp,270.84bp)  .. (2392.5bp,320.05bp);
   % Edge: Resolution_Compl_SC_Full -> Compactness
   \draw [->,-stealth,very thin] (1306.8bp,55.641bp) .. controls (1275.7bp,66.321bp) and (1241.2bp,80.506bp)  .. (1212.2bp,98.225bp) .. controls (1157.1bp,131.86bp) and (1146.3bp,146.72bp)  .. (1105.2bp,196.45bp) .. controls (1074.8bp,233.16bp) and (1047.2bp,281.23bp)  .. (1026.6bp,319.96bp);
   % Edge: CNF_Formulas_Sema -> CNF_Sema
   \draw [->,-stealth,very thin] (2773.1bp,256.14bp) .. controls (2798.3bp,274.21bp) and (2830.6bp,297.3bp)  .. (2863.0bp,320.46bp);
   % Edge: Resolution_Sound -> Resolution
   \draw [->,-stealth,very thin] (2754.5bp,147.13bp) .. controls (2787.8bp,163.92bp) and (2837.9bp,189.11bp)  .. (2882.0bp,211.37bp);
   % Edge: HC_Compl_Consistency -> HC
   \draw [->,-stealth,very thin] (1747.1bp,255.83bp) .. controls (1734.5bp,266.54bp) and (1722.0bp,279.78bp)  .. (1714.2bp,294.68bp) .. controls (1695.4bp,330.39bp) and (1692.8bp,377.83bp)  .. (1693.8bp,418.04bp);
   % Edge: ND_Compl_SC -> SCND
   \draw [->,-stealth,very thin] (641.44bp,258.77bp) .. controls (647.27bp,274.96bp) and (654.35bp,294.59bp)  .. (663.52bp,320.03bp);
   % Edge: Sema -> Formulas
   \draw [->,-stealth,very thin] (1567.4bp,449.5bp) .. controls (1610.9bp,461.28bp) and (1676.0bp,478.89bp)  .. (1734.2bp,494.63bp);
   % Edge: Substitution_Sema -> Substitution
   \draw [->,-stealth,very thin] (1842.6bp,356.99bp) .. controls (1850.1bp,371.67bp) and (1860.6bp,392.43bp)  .. (1873.8bp,418.35bp);
   % Edge: HC_Compl_Consistency -> Consistency
   \draw [->,-stealth,very thin] (1730.6bp,252.74bp) .. controls (1693.3bp,269.02bp) and (1644.5bp,290.32bp)  .. (1595.6bp,311.7bp);
   % Edge: Substitution -> Formulas
   \draw [->,-stealth,very thin] (1860.4bp,454.36bp) .. controls (1848.5bp,463.61bp) and (1833.7bp,475.08bp)  .. (1812.4bp,491.55bp);
   % Edge: Resolution_Compl_SC_Full -> LSC_Resolution
   \draw [->,-stealth,very thin] (1495.9bp,52.608bp) .. controls (1582.1bp,70.801bp) and (1703.7bp,96.485bp)  .. (1791.8bp,115.1bp);
   % Edge: Resolution_Compl -> CNF_Sema
   \draw [->,-stealth,very thin] (3059.8bp,160.26bp) .. controls (3043.6bp,187.74bp) and (3017.6bp,228.16bp)  .. (2989.2bp,258.68bp) .. controls (2969.6bp,279.72bp) and (2944.2bp,299.77bp)  .. (2915.3bp,320.5bp);
   % Edge: Resolution_Compl_SC_Full -> SC_Sema
   \draw [->,-stealth,very thin] (1254.9bp,34.382bp) .. controls (960.97bp,41.962bp) and (301.53bp,62.837bp)  .. (268.19bp,98.225bp) .. controls (219.29bp,150.13bp) and (244.55bp,191.4bp)  .. (268.19bp,258.68bp) .. controls (275.39bp,279.18bp) and (290.33bp,298.32bp)  .. (311.34bp,320.21bp);
   % Edge: Compactness_Consistency -> Consistency
   \draw [->,-stealth,very thin] (1534.2bp,258.77bp) .. controls (1534.2bp,270.58bp) and (1534.2bp,284.23bp)  .. (1534.2bp,307.16bp);
   % Edge: ND_Sound -> Sema
   \draw [->,-stealth,very thin] (861.84bp,355.92bp) .. controls (879.98bp,365.38bp) and (903.73bp,376.34bp)  .. (926.19bp,382.36bp) .. controls (1022.3bp,408.11bp) and (1308.7bp,425.84bp)  .. (1456.0bp,433.63bp);
   % Edge: LSC_Resolution -> LSC
   \draw [->,-stealth,very thin] (1776.6bp,140.89bp) .. controls (1689.1bp,153.42bp) and (1547.1bp,174.56bp)  .. (1425.2bp,196.45bp) .. controls (1412.4bp,198.75bp) and (1399.0bp,201.28bp)  .. (1375.7bp,205.88bp);
   % Edge: Resolution_Compl -> Resolution
   \draw [->,-stealth,very thin] (3028.7bp,158.54bp) .. controls (3003.7bp,173.62bp) and (2973.7bp,191.71bp)  .. (2941.9bp,210.87bp);
   % Edge: SC_Sema -> SC
   \draw [->,-stealth,very thin] (367.59bp,356.08bp) .. controls (400.67bp,372.49bp) and (450.19bp,397.05bp)  .. (495.1bp,419.33bp);
   % Edge: ND_Compl_Truthtable -> ND_Sound
   \draw [->,-stealth,very thin] (862.1bp,258.77bp) .. controls (855.82bp,274.96bp) and (848.21bp,294.59bp)  .. (838.35bp,320.03bp);
   % Edge: Consistency -> Sema
   \draw [->,-stealth,very thin] (1529.7bp,369.87bp) .. controls (1528.0bp,382.2bp) and (1526.0bp,396.26bp)  .. (1522.8bp,418.25bp);
   % Edge: Resolution_Sound -> CNF_Formulas_Sema
   \draw [->,-stealth,very thin] (2721.8bp,147.81bp) .. controls (2723.4bp,158.71bp) and (2725.4bp,172.95bp)  .. (2728.7bp,196.42bp);
   % Edge: ND_Sound -> ND
   \draw [->,-stealth,very thin] (831.19bp,356.99bp) .. controls (831.19bp,371.4bp) and (831.19bp,391.66bp)  .. (831.19bp,418.35bp);
   % Edge: Resolution_Compl_SC_Small -> CNF_Formulas_Sema
   \draw [->,-stealth,very thin] (2224.5bp,46.318bp) .. controls (2341.5bp,56.742bp) and (2468.8bp,73.289bp)  .. (2521.2bp,98.225bp) .. controls (2557.3bp,115.42bp) and (2553.1bp,138.0bp)  .. (2586.2bp,160.45bp) .. controls (2608.9bp,175.88bp) and (2635.8bp,189.33bp)  .. (2669.6bp,204.03bp);
   % Edge: CNF_Sema -> CNF
   \draw [->,-stealth,very thin] (2862.9bp,356.53bp) .. controls (2839.6bp,373.08bp) and (2805.1bp,397.63bp)  .. (2772.2bp,421.11bp);
   % Edge: HC -> Formulas
   \draw [->,-stealth,very thin] (1718.4bp,454.73bp) .. controls (1730.3bp,463.91bp) and (1744.9bp,475.22bp)  .. (1765.9bp,491.48bp);
   % Edge: Resolution_Compl_Consistency -> Resolution
   \draw [->,-stealth,very thin] (2494.7bp,145.88bp) .. controls (2524.1bp,150.7bp) and (2556.5bp,155.9bp)  .. (2586.2bp,160.45bp) .. controls (2698.5bp,177.63bp) and (2729.6bp,166.45bp)  .. (2839.2bp,196.45bp) .. controls (2849.9bp,199.39bp) and (2861.1bp,203.47bp)  .. (2880.8bp,211.62bp);
   % Edge: MiniFormulas_Sema -> MiniFormulas
   \draw [->,-stealth,very thin] (2092.8bp,382.46bp) .. controls (2091.8bp,391.03bp) and (2090.7bp,399.81bp)  .. (2088.5bp,417.94bp);
   % Edge: Tseytin_Sema -> Tseytin
   \draw [->,-stealth,very thin] (1472.3bp,139.25bp) .. controls (1670.1bp,155.45bp) and (2044.5bp,186.75bp)  .. (2105.2bp,196.45bp) .. controls (2125.9bp,199.75bp) and (2148.1bp,204.44bp)  .. (2178.2bp,211.5bp);
   % Edge: SC_Compl_Consistency -> Consistency
   \draw [->,-stealth,very thin] (480.03bp,249.92bp) .. controls (492.94bp,253.36bp) and (506.39bp,256.48bp)  .. (519.19bp,258.68bp) .. controls (777.69bp,302.93bp) and (846.8bp,273.25bp)  .. (1108.2bp,294.68bp) .. controls (1211.7bp,303.16bp) and (1329.1bp,315.45bp)  .. (1424.4bp,325.96bp);
   % Edge: CNF_Formulas_Sema -> Sema
   \draw [->,-stealth,very thin] (2665.6bp,249.9bp) .. controls (2652.9bp,253.36bp) and (2639.8bp,256.51bp)  .. (2627.2bp,258.68bp) .. controls (2557.3bp,270.74bp) and (2048.3bp,254.11bp)  .. (1990.2bp,294.68bp) .. controls (1955.4bp,318.98bp) and (1986.5bp,357.3bp)  .. (1952.2bp,382.36bp) .. controls (1887.6bp,429.53bp) and (1673.0bp,404.68bp)  .. (1594.2bp,418.36bp) .. controls (1588.7bp,419.31bp) and (1583.1bp,420.44bp)  .. (1567.3bp,423.96bp);
   % Edge: SC_Depth_Limit -> SC_Sema
   \draw [->,-stealth,very thin] (162.7bp,254.56bp) .. controls (200.98bp,273.52bp) and (251.55bp,298.57bp)  .. (296.72bp,320.95bp);
   % Edge: ND_Compl_SC -> ND_Sound
   \draw [->,-stealth,very thin] (679.61bp,254.85bp) .. controls (713.79bp,273.71bp) and (758.69bp,298.5bp)  .. (799.82bp,321.2bp);
   % Node: Resolution_Compl_Consistency
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2396.19bp,134.54bp) node {Resolution complete};
   \draw (2396.19bp,116.54bp) node {(via Consistency)};
 \end{scope}
   % Node: ND_Compl_SC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (630.19bp,232.76bp) node {ND completeness};
   \draw (630.19bp,214.76bp) node {(via SC)};
 \end{scope}
   % Node: CNF_Formulas
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2392.2bp,338.52bp) node {Formulas in CNF};
 \end{scope}
   % Node: Substitution_Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1833.2bp,338.52bp) node {Substitution lemma};
 \end{scope}
   % Node: CNF_Formulas_Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (2733.19bp,232.76bp) node {Formulas→CNF:};
+  \draw (2733.19bp,232.76bp) node {Formulas$\rightarrow$CNF:};
   \draw (2733.19bp,214.76bp) node {correctness};
 \end{scope}
   % Node: LSC_Resolution
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (1859.2bp,129.34bp) node {LSC ↔ Resolution};
+  \draw (1859.2bp,129.34bp) node {LSC $\leftrightarrow$ Resolution};
 \end{scope}
   % Node: HC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1695.2bp,436.74bp) node {Hilbert Calculus};
 \end{scope}
   % Node: SCND
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (670.19bp,338.52bp) node {SC→ND};
+  \draw (670.19bp,338.52bp) node {SC$\rightarrow$ND};
 \end{scope}
   % Node: Formulas
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1789.2bp,509.51bp) node {Formula Syntax};
 \end{scope}
   % Node: SC_Compl_Consistency
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (410.19bp,232.76bp) node {SC complete};
   \draw (410.19bp,214.76bp) node {(via Consistency)};
 \end{scope}
   % Node: ND
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (831.19bp,436.74bp) node {Natural Deduction};
 \end{scope}
   % Node: Tseytin
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2239.2bp,227.56bp) node {Tseytin transformation};
 \end{scope}
   % Node: MiniFormulas
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (2086.2bp,436.74bp) node {→ only formulas};
+  \draw (2086.2bp,436.74bp) node {$\rightarrow$ only formulas};
 \end{scope}
   % Node: ND_Compl_Truthtable_Compact
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (904.19bp,134.54bp) node {ND completeness};
   \draw (904.19bp,116.54bp) node {(generalized)};
 \end{scope}
   % Node: Substitution
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1883.2bp,436.74bp) node {Substitutions};
 \end{scope}
   % Node: ND_Sound
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (831.19bp,338.52bp) node {ND soundness};
 \end{scope}
   % Node: Resolution_Compl_SC_Small
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1988.19bp,36.31bp) node {Resolution completeness via LSC};
   \draw (1988.19bp,18.31bp) node {(using semantic correctness of formula CNF trans.)};
 \end{scope}
   % Node: CNF_To_Formula
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2519.19bp,232.76bp) node {Converting CNFs};
   \draw (2519.19bp,214.76bp) node {back to formulas};
 \end{scope}
   % Node: Sema_Craig
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2000.19bp,232.76bp) node {Interpolation};
   \draw (2000.19bp,214.76bp) node {using Semantics};
 \end{scope}
   % Node: MiniFormulas_Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2098.19bp,352.72bp) node {proof that};
-  \draw (2098.19bp,334.72bp) node {→ transformation};
+  \draw (2098.19bp,334.72bp) node {$\rightarrow$ transformation};
   \draw (2098.19bp,316.72bp) node {is sound};
 \end{scope}
   % Node: ND_Compl_Truthtable
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (874.19bp,232.76bp) node {ND completeness};
   \draw (874.19bp,214.76bp) node {(simulates truthtables)};
 \end{scope}
   % Node: Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1520.2bp,436.74bp) node {Semantics};
 \end{scope}
   % Node: CNF
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2750.2bp,436.74bp) node {CNFs};
 \end{scope}
   % Node: SC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (530.19bp,436.74bp) node {Sequent Calculus};
 \end{scope}
   % Node: CNF_Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2888.2bp,338.52bp) node {Semantics of CNFs};
 \end{scope}
   % Node: Compactness
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1017.2bp,338.52bp) node {Compactness};
 \end{scope}
   % Node: SC_Depth_Limit
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (108.19bp,232.76bp) node {SC derivations and};
   \draw (108.19bp,214.76bp) node {a limit for depth};
 \end{scope}
   % Node: Consistency
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1534.19bp,343.72bp) node {Abstract Consistency};
   \draw (1534.19bp,325.72bp) node {Properties};
 \end{scope}
   % Node: Resolution_Compl
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (3077.19bp,134.54bp) node {Resolution completeness};
   \draw (3077.19bp,116.54bp) node {(induction over atom set)};
 \end{scope}
   % Node: Resolution_Sound
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2719.2bp,129.34bp) node {Resolution soundness};
 \end{scope}
   % Node: Resolution
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (2914.2bp,227.56bp) node {Resolution};
 \end{scope}
   % Node: LSC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1273.19bp,232.76bp) node {Transforming SC: to CNF,};
   \draw (1273.19bp,214.76bp) node {to left handed SC (LSC)};
 \end{scope}
   % Node: SC_Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (332.19bp,338.52bp) node {SC sound/complete};
 \end{scope}
   % Node: Resolution_Compl_SC_Full
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1394.19bp,36.31bp) node {Resolution completeness};
   \draw (1394.19bp,18.31bp) node {via LSC};
 \end{scope}
   % Node: SC_Depth
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (111.19bp,343.72bp) node {SC derivations};
   \draw (111.19bp,325.72bp) node {and depth};
 \end{scope}
   % Node: HC_Compl_Consistency
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1788.19bp,232.76bp) node {HC complete};
   \draw (1788.19bp,214.76bp) node {(via consistency)};
 \end{scope}
   % Node: Compactness_Consistency
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1534.19bp,232.76bp) node {Compactness};
   \draw (1534.19bp,214.76bp) node {(via Consistency)};
 \end{scope}
   % Node: Tseytin_Sema
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1350.19bp,134.54bp) node {Tseytin transformation:};
   \draw (1350.19bp,116.54bp) node {correctness};
 \end{scope}
   % Node: SC_Cut
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (530.19bp,343.72bp) node {SC: cut};
   \draw (530.19bp,325.72bp) node {contraction};
 \end{scope}
 %
 \end{tikzpicture}
 
diff --git a/thys/Propositional_Proof_Systems/document/fig_tran.tex b/thys/Propositional_Proof_Systems/document/fig_tran.tex
--- a/thys/Propositional_Proof_Systems/document/fig_tran.tex
+++ b/thys/Propositional_Proof_Systems/document/fig_tran.tex
@@ -1,212 +1,212 @@
 
 \begin{tikzpicture}[>=latex,line join=bevel,scale=0.15, every node/.style={scale=0.3}]
   \pgfsetlinewidth{1bp}
 %%
 \pgfsetcolor{black}
   % Edge: ND -> Formulas
   \draw [->,-stealth,very thin] (347.07bp,268.93bp) .. controls (418.11bp,290.17bp) and (548.78bp,328.42bp)  .. (661.45bp,356.9bp) .. controls (718.33bp,371.28bp) and (783.18bp,385.64bp)  .. (841.51bp,398.07bp);
   % Edge: MiniSC_HC -> MiniSC
   \draw [->,-stealth,very thin] (627.78bp,171.68bp) .. controls (658.89bp,185.38bp) and (703.61bp,205.08bp)  .. (750.65bp,225.8bp);
   % Edge: SC_Depth_Limit -> SC_Depth
   \draw [->,-stealth,very thin] (1383.3bp,182.94bp) .. controls (1363.9bp,194.79bp) and (1341.2bp,208.65bp)  .. (1312.4bp,226.22bp);
   % Edge: SCND -> ND
   \draw [->,-stealth,very thin] (84.793bp,170.22bp) .. controls (95.352bp,175.41bp) and (107.34bp,181.1bp)  .. (118.45bp,185.91bp) .. controls (158.09bp,203.06bp) and (203.67bp,220.38bp)  .. (248.05bp,236.6bp);
   % Edge: MiniSC_HC -> HC
   \draw [->,-stealth,very thin] (587.0bp,173.27bp) .. controls (585.1bp,187.68bp) and (582.41bp,207.94bp)  .. (578.88bp,234.63bp);
   % Edge: SC_Gentzen -> SC_Cut
   \draw [->,-stealth,very thin] (1180.9bp,173.27bp) .. controls (1167.6bp,185.78bp) and (1149.7bp,202.71bp)  .. (1126.2bp,224.96bp);
   % Edge: MiniSC -> MiniFormulas
   \draw [->,-stealth,very thin] (818.31bp,284.37bp) .. controls (819.89bp,292.81bp) and (821.59bp,301.9bp)  .. (825.0bp,320.1bp);
   % Edge: LSC_Resolution -> Resolution
   \draw [->,-stealth,very thin] (1803.9bp,62.046bp) .. controls (1819.4bp,77.001bp) and (1839.6bp,99.58bp)  .. (1850.4bp,123.68bp) .. controls (1865.0bp,156.07bp) and (1868.9bp,197.18bp)  .. (1869.8bp,234.58bp);
   % Edge: CNF_Formulas -> CNF
   \draw [->,-stealth,very thin] (1707.5bp,271.15bp) .. controls (1720.9bp,283.81bp) and (1738.8bp,300.83bp)  .. (1760.9bp,321.86bp);
   % Edge: NDHC -> HC
   \draw [->,-stealth,very thin] (446.21bp,171.01bp) .. controls (471.77bp,187.11bp) and (511.2bp,211.94bp)  .. (548.54bp,235.45bp);
   % Edge: SCND -> SC
   \draw [->,-stealth,very thin] (65.886bp,173.15bp) .. controls (85.526bp,202.77bp) and (128.78bp,260.21bp)  .. (182.45bp,284.13bp) .. controls (258.65bp,318.1bp) and (849.28bp,313.48bp)  .. (932.45bp,320.13bp) .. controls (955.21bp,321.95bp) and (979.7bp,324.42bp)  .. (1012.7bp,328.09bp);
   % Edge: LSC -> SC_Cut
   \draw [->,-stealth,very thin] (1597.7bp,176.96bp) .. controls (1580.7bp,180.27bp) and (1563.1bp,183.41bp)  .. (1546.4bp,185.91bp) .. controls (1381.7bp,210.64bp) and (1335.2bp,182.3bp)  .. (1173.4bp,221.91bp) .. controls (1167.2bp,223.44bp) and (1160.8bp,225.38bp)  .. (1144.6bp,231.1bp);
   % Edge: MiniSC_Craig -> MiniSC
   \draw [->,-stealth,very thin] (929.22bp,172.81bp) .. controls (910.92bp,185.38bp) and (885.89bp,202.57bp)  .. (855.35bp,223.55bp);
   % Edge: SC_Depth -> SC
   \draw [->,-stealth,very thin] (1217.8bp,278.21bp) .. controls (1193.2bp,290.43bp) and (1163.9bp,304.96bp)  .. (1131.2bp,321.22bp);
   % Edge: MiniFormulas -> Formulas
   \draw [->,-stealth,very thin] (847.88bp,356.88bp) .. controls (857.25bp,365.74bp) and (868.64bp,376.5bp)  .. (886.29bp,393.18bp);
   % Edge: LSC -> CNF_Formulas
   \draw [->,-stealth,very thin] (1695.3bp,186.14bp) .. controls (1694.0bp,198.48bp) and (1692.6bp,212.54bp)  .. (1690.3bp,234.53bp);
   % Edge: SC_Cut -> SC
   \draw [->,-stealth,very thin] (1096.4bp,284.37bp) .. controls (1096.4bp,292.72bp) and (1096.4bp,301.7bp)  .. (1096.4bp,320.1bp);
   % Edge: SC -> Formulas
   \draw [->,-stealth,very thin] (1052.6bp,355.21bp) .. controls (1024.4bp,365.96bp) and (987.56bp,380.0bp)  .. (948.4bp,394.92bp);
   % Edge: HCSC -> SC_Cut
   \draw [->,-stealth,very thin] (787.51bp,170.54bp) .. controls (798.27bp,175.93bp) and (810.71bp,181.67bp)  .. (822.45bp,185.91bp) .. controls (859.27bp,199.2bp) and (956.98bp,222.07bp)  .. (1035.0bp,239.56bp);
   % Edge: HCSCND -> SCND
   \draw [->,-stealth,very thin] (311.24bp,67.3bp) .. controls (253.14bp,81.127bp) and (180.98bp,100.47bp)  .. (118.45bp,123.68bp) .. controls (109.95bp,126.84bp) and (101.06bp,130.74bp)  .. (83.557bp,139.16bp);
   % Edge: HCSCND -> HCSC
   \draw [->,-stealth,very thin] (524.61bp,69.739bp) .. controls (576.36bp,83.725bp) and (639.43bp,102.47bp)  .. (694.45bp,123.68bp) .. controls (702.82bp,126.91bp) and (711.6bp,130.81bp)  .. (728.96bp,139.17bp);
   % Edge: MiniSC_Craig -> Formulas
   \draw [->,-stealth,very thin] (956.06bp,173.24bp) .. controls (956.68bp,209.53bp) and (955.21bp,292.28bp)  .. (932.45bp,356.9bp) .. controls (929.29bp,365.86bp) and (925.01bp,375.25bp)  .. (916.12bp,392.65bp);
   % Edge: NDHC -> ND
   \draw [->,-stealth,very thin] (398.79bp,171.68bp) .. controls (378.61bp,187.41bp) and (348.3bp,211.04bp)  .. (317.53bp,235.03bp);
   % Edge: SC_Gentzen -> SC_Depth
   \draw [->,-stealth,very thin] (1213.2bp,173.27bp) .. controls (1221.2bp,184.77bp) and (1231.8bp,200.02bp)  .. (1247.4bp,222.66bp);
   % Edge: Resolution -> CNF
   \draw [->,-stealth,very thin] (1850.6bp,270.73bp) .. controls (1837.0bp,283.48bp) and (1818.6bp,300.81bp)  .. (1796.3bp,321.7bp);
   % Edge: HCSC -> HC
   \draw [->,-stealth,very thin] (729.21bp,170.58bp) .. controls (699.08bp,186.83bp) and (651.86bp,212.32bp)  .. (608.68bp,235.62bp);
   % Edge: ND_FiniteAssms -> ND
   \draw [->,-stealth,very thin] (255.33bp,185.6bp) .. controls (262.77bp,198.43bp) and (271.33bp,213.19bp)  .. (283.77bp,234.62bp);
   % Edge: LSC_Resolution -> LSC
   \draw [->,-stealth,very thin] (1769.4bp,62.162bp) .. controls (1758.3bp,76.681bp) and (1742.4bp,97.482bp)  .. (1722.2bp,123.85bp);
   % Edge: HCSCND -> NDHC
   \draw [->,-stealth,very thin] (420.45bp,87.692bp) .. controls (420.45bp,100.68bp) and (420.45bp,114.55bp)  .. (420.45bp,136.39bp);
   % Edge: MiniSC -> SC
   \draw [->,-stealth,very thin] (892.69bp,277.18bp) .. controls (937.49bp,290.66bp) and (992.47bp,307.21bp)  .. (1043.7bp,322.65bp);
   % Edge: CNF_Formulas -> Formulas
   \draw [->,-stealth,very thin] (1625.8bp,267.22bp) .. controls (1534.0bp,287.88bp) and (1357.4bp,327.01bp)  .. (1206.4bp,356.9bp) .. controls (1131.7bp,371.71bp) and (1046.2bp,387.0bp)  .. (975.52bp,399.31bp);
   % Edge: HC -> Formulas
   \draw [->,-stealth,very thin] (597.62bp,271.22bp) .. controls (625.18bp,294.08bp) and (675.59bp,333.18bp)  .. (724.45bp,356.9bp) .. controls (758.7bp,373.53bp) and (799.09bp,386.26bp)  .. (842.86bp,397.74bp);
   % Node: HCSC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (758.45bp,154.79bp) node {HC→SC};
+  \draw (758.45bp,154.79bp) node {HC$\rightarrow$SC};
 \end{scope}
   % Node: HCSCND
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (420.45bp,58.04bp) node {Single Formula};
   \draw (420.45bp,40.04bp) node {provability equivalence};
-  \draw (420.45bp,22.04bp) node {HC↔ND↔SC};
+  \draw (420.45bp,22.04bp) node {HC$\leftrightarrow$ND$\leftrightarrow$SC};
 \end{scope}
   % Node: SC_Gentzen
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1200.4bp,154.79bp) node {Gentzen Style SC};
 \end{scope}
   % Node: HC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (576.45bp,253.02bp) node {Hilbert Calculus};
 \end{scope}
   % Node: LSC_Resolution
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (1783.4bp,43.841bp) node {LSC ↔ Resolution};
+  \draw (1783.4bp,43.841bp) node {LSC $\leftrightarrow$ Resolution};
 \end{scope}
   % Node: SCND
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (54.447bp,154.79bp) node {SC→ND};
+  \draw (54.447bp,154.79bp) node {SC$\rightarrow$ND};
 \end{scope}
   % Node: Formulas
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (905.45bp,411.29bp) node {Formula Syntax};
 \end{scope}
   % Node: LSC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1698.45bp,159.99bp) node {Transforming SC: to CNF,};
   \draw (1698.45bp,141.99bp) node {to left handed SC (LSC)};
 \end{scope}
   % Node: ND
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (294.45bp,253.02bp) node {Natural Deduction};
 \end{scope}
   % Node: MiniFormulas
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (828.45bp,338.52bp) node {→ only formulas};
+  \draw (828.45bp,338.52bp) node {$\rightarrow$ only formulas};
 \end{scope}
   % Node: MiniSC_HC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (589.45bp,154.79bp) node {→ only: SC→HC};
+  \draw (589.45bp,154.79bp) node {$\rightarrow$ only: SC$\rightarrow$HC};
 \end{scope}
   % Node: NDHC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (420.45bp,154.79bp) node {ND→HC};
+  \draw (420.45bp,154.79bp) node {ND$\rightarrow$HC};
 \end{scope}
   % Node: CNF
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1778.4bp,338.52bp) node {CNFs};
 \end{scope}
   % Node: MiniSC_Craig
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (955.45bp,154.79bp) node {Interpolation using SC};
 \end{scope}
   % Node: SC_Depth_Limit
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1429.45bp,159.99bp) node {SC derivations and};
   \draw (1429.45bp,141.99bp) node {a limit for depth};
 \end{scope}
   % Node: Resolution
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1869.4bp,253.02bp) node {Resolution};
 \end{scope}
   % Node: ND_FiniteAssms
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (237.45bp,159.99bp) node {ND and a dead end};
   \draw (237.45bp,141.99bp) node {to compactness};
 \end{scope}
   % Node: CNF_Formulas
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1688.4bp,253.02bp) node {Formulas in CNF};
 \end{scope}
   % Node: SC_Depth
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1268.45bp,258.22bp) node {SC derivations};
   \draw (1268.45bp,240.22bp) node {and depth};
 \end{scope}
   % Node: MiniSC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
-  \draw (812.45bp,258.22bp) node {→ only transformation:};
+  \draw (812.45bp,258.22bp) node {$\rightarrow$ only transformation:};
   \draw (812.45bp,240.22bp) node {SC invariant};
 \end{scope}
   % Node: SC
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1096.4bp,338.52bp) node {Sequent Calculus};
 \end{scope}
   % Node: SC_Cut
 \begin{scope}
   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
   \pgfsetstrokecolor{strokecol}
   \draw (1096.45bp,258.22bp) node {SC: cut};
   \draw (1096.45bp,240.22bp) node {contraction};
 \end{scope}
 %
 \end{tikzpicture}
 
diff --git a/thys/Propositional_Proof_Systems/document/root.tex b/thys/Propositional_Proof_Systems/document/root.tex
--- a/thys/Propositional_Proof_Systems/document/root.tex
+++ b/thys/Propositional_Proof_Systems/document/root.tex
@@ -1,92 +1,90 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 
 \usepackage[x11names, rgb]{xcolor}
 \usepackage[utf8]{inputenc}
 \usepackage{tikz}
 \usetikzlibrary{snakes,arrows,shapes}
 \usepackage{amsmath}
-\DeclareUnicodeCharacter{2192}{$\rightarrow$}
-\DeclareUnicodeCharacter{2194}{$\leftrightarrow$}
 
 % 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>
 
 %\renewcommand{\isasymdots}{\dots}
 
 % 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}
 
 \begin{document}
 
 \title{Propositional Proof Systems}
 \author{Julius Michaelis and Tobias Nipkow}
 \maketitle
 \begin{abstract}
 We present a formalization of Sequent Calculus, Natural Deduction, Hilbert Calculus, and Resolution using a deep embedding of propositional formulas. 
 We provide proofs of many of the classical results, including Cut Elimination, Craig's Interpolation, proof transformation between all calculi, and soundness and completeness.
 Additionally, we formalize the Model Existence Theorem.
 \end{abstract}
 
 \tableofcontents
 \vspace{1em}
 
 The files of this entry are organized as a web of results that should allow loading only that part of the formalization that the user is interested in.
 Special care was taken not to mix proofs that require semanics and proofs that talk about transformation between proof systems.
 An overview of the different theory files and their dependencies can be found in figures \ref{fig:prooftran} and \ref{fig:sema}.
 
 % ./overview.sh tex sema >document/fig_sema.tex && ./overview.sh tex prooftran >document/fig_tran.tex
 \begin{figure}
 	\centering
 	\input{fig_tran}
 	\caption{Overview of results considering Proof Transformation}
 	\label{fig:prooftran}
 \end{figure}
 \begin{figure}
 	\centering
 	\scalebox{0.8}{\input{fig_sema}}
 	\caption{Overview of results considering Semantics}
 	\label{fig:sema}
 \end{figure}
 
 % 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:
diff --git a/thys/Sturm_Sequences/document/root_userguide.tex b/thys/Sturm_Sequences/document/root_userguide.tex
--- a/thys/Sturm_Sequences/document/root_userguide.tex
+++ b/thys/Sturm_Sequences/document/root_userguide.tex
@@ -1,147 +1,146 @@
 \documentclass[11pt,a4paper,oneside]{article}
 \usepackage[english]{babel}
 
 \usepackage[utf8x]{inputenc} 
 \usepackage[T1]{fontenc}
 
 \usepackage{geometry} 
 \usepackage{color} 
 \usepackage{graphicx} 
 \usepackage{pifont} 
 \usepackage[babel]{csquotes}
 \usepackage{textcomp}
 \usepackage{upgreek}
 \usepackage{amsmath}
 \usepackage{textcomp}
 \usepackage{amssymb}
 \usepackage{latexsym}
 \usepackage{pgf}
 \usepackage{nicefrac}
 \usepackage{enumerate}
 \usepackage{stmaryrd}
 
 \usepackage{tgpagella}
 
 \DeclareFontFamily{OT1}{pzc}{}
 \DeclareFontShape{OT1}{pzc}{m}{it}{<-> s * [1.10] pzcmi7t}{}
 \DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
-\DeclareUnicodeCharacter{10230}{$\rightarrow$}
 
 \newcommand{\ie}{i.\,e.}
 \newcommand{\wuppdi}[0]{\hfill\ensuremath{\square}}
 \newcommand{\qed}[0]{\vspace{-3mm}\begin{flushright}\textit{q.e.d.}\end{flushright}\vspace{3mm}}
 \newcommand{\bred}{\ensuremath{\longrightarrow_\beta}}
 \newcommand{\acos}{\textrm{arccos}}
 \newcommand{\determ}[1]{\textrm{det}(#1)}
 \newcommand{\RR}{\mathbb{R}}
 \newcommand{\BB}{\mathbb{B}}
 \newcommand{\NN}{\mathbb{N}}
 \newcommand{\QQ}{\mathbb{Q}}
 \newcommand{\ZZ}{\mathbb{Z}}
 \newcommand{\CC}{\mathbb{C}}
 \newcommand{\II}{\mathbb{I}}
 \newcommand{\kernel}[1]{\textrm{ker}(#1)}
 \renewcommand{\epsilon}{\varepsilon}
 \renewcommand{\phi}{\varphi}
 \renewcommand{\theta}{\vartheta}
 \newcommand{\atan}{\mathrm{arctan}}
 \newcommand{\rot}{\mathrm{rot}}
 \newcommand{\vdiv}{\mathrm{div}}
 \newcommand{\shouldbe}{\stackrel{!}{=}}
 \newcommand{\sturm}{\texttt{sturm}}
 \newcommand{\lemma}{\textbf{lemma}}
 \newcommand{\card}{\textrm{card}}
 \newcommand{\real}{\textrm{real}}
 
 \newcommand{\isabellehol}{\mbox{Isabelle}\slash HOL}
 
 \geometry{a4paper,left=30mm,right=30mm, top=25mm, bottom=30mm} 
 
 \title{\LARGE User's Guide for the \texttt{sturm} Method\\[4mm]}
 \author{\Large Manuel Eberl <eberlm@in.tum.de>\\[1mm]\large Institut für Informatik, Technische Universität München\\[4mm]}
 
 \begin{document}
 \begin{center}
 \vspace*{20mm}
 \includegraphics[width=4cm]{isabelle.pdf}
 \end{center}
 \vspace*{-5mm}
 {\let\newpage\relax\maketitle}
 \vspace*{10mm}
 \tableofcontents
 \newpage
 
 \section{Introduction}
 
 The \sturm\ method uses Sturm's theorem to determine the number of distinct real roots of a polynomial (with rational coefficients) within a certain interval. It also provides some preprocessing to decide a number of statements that can be reduced to real roots of polynomials, such as simple polynomial inequalities and logical combinations of polynomial equations.
 \vspace*{10mm}
 
 \section{Usage}
 
 \subsection{Examples}
 The following examples should give a good overview of what the \sturm\ method can do:
 \begin{align*}
 &\lemma\ "\card\ \{x::\real.\ (x - 1)^2 * (x + 1) = 0\}\  =\  2"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "\mathrm{card}\ \{x::\mathrm{real}.\ -0.010831 < x\ \wedge\ x < 0.010831\ \wedge\\
 &\hskip20mm \mathrm{poly}\ [:0, -17/2097152, -49/16777216, 1/6, 1/24, 1/120:]\ \ x\ =\ 0\}\  =\  3"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "\card\ \{x::\real.\ x^3 + x = 2*x^2\ \wedge\ x^3-6*x^2+11*x=6\}\  =\  1"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "\card\ \{x::\real.\ x^3 + x = 2*x^2\ \vee\ x^3-6*x^2+11*x=6\}\  =\  4"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "(x::\real)^2+1 > 0"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "(x::\real) > 0\ \Longrightarrow\ x^2+1 > 0"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "\llbracket (x::\real) > 0; x \leq 2/3\rrbracket\ \Longrightarrow\ x*x \neq\ x"\ \textrm{\textbf{by}\ sturm}\\
 &\lemma\ "(x::\real) > 1\ \Longrightarrow\ x*x > x"\ \textrm{\textbf{by}\ sturm}\\
 \end{align*}
 
 \subsection{Determining the number of real roots}
 The \enquote{classical} application of Sturm's theorem is to count the number of real roots of a polynomial in a certain interval. The \sturm\ method supports this for any polynomial with rational coefficients and any real interval, \ie $[a;b]$, $(a;b]$, $[a;b)$, and $(a;b)$ where $a\in\QQ\cup\{-\infty\}$ and $b\in\QQ\cup\{\infty\}$.\footnote{The restriction to rational numbers for the coefficients and interval bounds is to the fact that the code generator is used internally, which, of course, does not support computations on irrational real numbers.} The general form of the theorems the method expects is:
 $$\card\ \{x::\real.\ a < x \wedge x < b \wedge p\ x = 0\}\ =\ ?n$$
 $?n$ should be replaced by the actual number of such roots and $p$ may be any polynomial real function in $x$ with rational coefficients. The bounds $a < x$ and $x < b$ can be omitted for the \enquote{$\infty$} case.\\
 
 Furthermore, the \sturm\ method can instantiate the number $?n$ on the right-hand side automatically if it is left unspecified (as a schematic variable in a schematic lemma). However, due to technical restrictions this also takes twice as long as simply proving that the specified number is correct.
 
 \newpage
 \subsection{Inequalities}
 
 A simple special case of root counting is the statement that a polynomial $p\in\RR[X]$ has no roots in a certain interval, which can be written as:
 $$\forall x::\real.\ x > a \wedge x < b \longrightarrow p\ x \neq 0$$
 The \sturm\ method can be directly applied to statements such as this and prove them.
 
 \subsection{More complex expressions}
 
 By using some simple preprocessing, the \sturm\ method can also decide more complex statements:
 $$\card\ \{x::\real.\ x > a\ \wedge\ x < b\ \wedge\ P\ x\}\ =\ n$$
 where $P\ x$ is a \enquote{polynomial expression}, which is defined as:
 \begin{enumerate}
 \item $p\ x= q\ x$, where $p$ and $q$ are polynomial functions, such as $\lambda x.\ a$, $\lambda x.\ x$, $\lambda x.\ x^2$, $\mathrm{poly}\ p$, and so on
 \item $P\ x\ \wedge\ Q\ x$ or $P\ x\ \vee\ Q\ x$, where $P\ x$ and $Q\ x$ are polynomial expressions
 \end{enumerate}
 
 Of course, by reduction to the case of zero roots, the following kind of statement is also provable by \sturm\ :
 $$\forall x::\real.\ x > a\ \wedge\ x < b\ \longrightarrow\ P\ x$$
 where $P\ x$ is a \enquote{negated polynomial expression}, which is defined as:
 \begin{enumerate}
 \item $p\ x\neq q\ x$, where $p$ and $q$ are polynomial functions
 \item $P\ x\ \wedge\ Q\ x$ or $P\ x\ \vee\ Q\ x$, where $P\ x$ and $Q\ x$ are negated polynomial expressions
 \end{enumerate}
 
 \subsection{Simple ordered inequalities}
 For any polynomial $p\in\RR[X]$, the question whether $p(x) > 0$ for all $x\in I$ for a non-empty real interval $I$ can obviously be reduced to the question of whether $p(x) \neq 0$ for all $x\in I$, \ie $p$ has no roots in $I$, and $p(x) > 0$ for some arbitrary fixed $x\in I$, the first of which can be decided using Sturm's theorem and the second by choosing an arbitrary $x\in I$ and evaluating $p(x)$.\\
 
 Using this reduction, the \sturm\ method can also decide single \enquote{less than}/\enquote{greater than} inequalities of the form 
 $$\forall x::\real.\ x > a\ \wedge\ x < b\ \longrightarrow\ p\ x < q\ x$$
 
 \subsection{A note on meta logic versus object logic}
 
 While statements like $\forall x::\real.\ x^2+1>0$ were expressed in their HOL notation in this guide, the \sturm\ method can also prove the meta logic equivalents $\bigwedge x::\real.\ x^2+1>0$ and $(x::\real)^2+1>0$ directly.
 
 \section{Troubleshooting}
 
 Should you find that the \sturm\ method fails to prove a statement that it should, according to the above text, be able to prove, please go through the following steps:
 \begin{enumerate}
 \item ensure that your function is indeed a \emph{real} polynomial. Add an appropriate type annotation if necessary.
 \item use a computer algebra system to ensure that the property is indeed correct
 \item if this did not help, send the statement in question to \texttt{eberlm@in.tum.de}; it may be a bug in the preprocessing of the proof method.
 \end{enumerate}
 
 \end{document}