main.tex

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass{article}

\usepackage{etoolbox} % \undef, allow more math alphabets
\makeatletter
\def\new@mathgroup{\alloc@8\mathgroup\mathchardef\@cclvi}
\patchcmd{\document@select@group}{\sixt@@n}{\@cclvi}{}{}
\patchcmd{\select@group}{\sixt@@n}{\@cclvi}{}{}
\makeatother

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{tabularx}
\usepackage{hyperref} % \url
% \usepackage{afterpage} % insert blank page after current page
\usepackage{bbding}
\usepackage{stmaryrd}
\usepackage{xfrac}
\usepackage{cmll}
\usepackage{mathrsfs}
\usepackage{fourier-orns}
\usepackage{MnSymbol}
\undef\mathdollar % needed to prevent \mathdollar already defined error
\usepackage{wasysym}
\usepackage{enumitem} % \setlist
\usepackage{tikz}
\usetikzlibrary{arrows}

\usepackage{fontspec}
\newfontfamily\freeserif{FreeSerif}
\DeclareTextFontCommand{\texfreeserif}{\freeserif}

\setcounter{MaxMatrixCols}{20}  % allow bmatrix of more than 10 columns

\newcommand{\fist}{\large\lefthand\;\normalsize}
\newcommand{\interrobang}{\textbf{\large\textinterrobang\;\normalsize}}
\newcommand{\defeq}{\stackrel{\mathrm{def}}=}

\newcommand{\cat}{\mathbf}
\newcommand{\mat}{\mathbf}
\newcommand{\vect}{\mathbf}
\newcommand{\class}{\mathcal}
\newcommand{\struct}{\mathfrak}
\newcommand{\lie}{\mathfrak}
\newcommand{\thy}{\mathscr}
\newcommand{\xspace}{\mathsf}
\newcommand{\mono}{\mathtt}
\newcommand{\nats}{\mathbb{N}}
\newcommand{\primes}{\mathbb{P}}
\newcommand{\ints}{\mathbb{Z}}
\newcommand{\rats}{\mathbb{Q}}
\newcommand{\reals}{\mathbb{R}}
\newcommand{\comps}{\mathbb{C}}
\newcommand{\quats}{\mathbb{H}}
\newcommand{\octs}{\mathbb{O}}
\newcommand{\algs}{\mathbb{A}}
\newcommand{\prob}{\mathbb{P}}
\newcommand{\proj}{\mathsf{P}}  % projective spaces
\newcommand{\expect}{\mathbb{E}}
\newcommand{\cards}{\texfreeserif{\char1514}}
\newcommand{\ords}{\Omega}

% differential operator
\newcommand{\deriv}[2]{\frac{\mathrm{d}#1}{\mathrm{d}#2}}
\newcommand{\pderiv}[2]{\frac{\partial{#1}}{\partial{#2}}}
\newcommand{\diffy}[1]{\mathrm{d}#1}
\newcommand{\diffint}{\mathbb{D}}

\newcommand{\pow}{\mathscr{P}}
\newcommand{\Spec}{\mathrm{Spec}}
\newcommand{\Frac}{\mathrm{Frac}}

\newcommand{\One}{\mathbf{1}}
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\Id}{\mathrm{Id}}
\newcommand{\Nat}{\mathsf{Nat}}
\newcommand{\Unit}{\mathsf{Unit}}
\newcommand{\unit}{\mathsf{unit}}
\newcommand{\End}{\mathsf{End}}
\newcommand{\suc}{\mathsf{suc}}
\newcommand{\pred}{\mathsf{pred}}
\newcommand{\fst}{\mathsf{fst}}
\newcommand{\snd}{\mathsf{snd}}
\newcommand{\ctx}{\;\mathrm{ctx}}
\newcommand{\prop}{\;\mathrm{prop}}
\newcommand{\Prop}{\mathsf{Prop}}
\newcommand{\type}{\;\mathrm{type}}
\newcommand{\Type}{\mathsf{Type}}
\newcommand{\hastypef}{\mono{\;'\kern-3pt:}\;}
\newcommand{\eff}{\text{\emph{eff}}}
\newcommand{\case}{\mono{case}}
\newcommand{\of}{\mono{of}}
\newcommand{\rec}{\mono{rec}}
\newcommand{\lett}{\mono{let}}
\newcommand{\inn}{\mono{in}}
\newcommand{\callcc}{\mono{callcc}}
\newcommand{\callCC}{\mathsf{callCC}}
\newcommand{\bindop}{\mathsf{\gg\kern-3pt=}}
\newcommand{\altop}{\mathsf{\;:\kern-3pt+\;}}
\newcommand{\minlozenge}{\mathrlap{-}\lozenge}
%\newcommand{\diamondplus}{\mathrlap{+}\Diamond}
\newcommand{\llense}{[\kern-1.95pt(}
\newcommand{\rlense}{)\kern-2.0pt]}
\newcommand{\until}{\mathsf{U}}
\newcommand{\untileq}{\underline{\mathsf{U}}}
\newcommand{\since}{\mathsf{S}}
\newcommand{\sinceeq}{\underline{\mathsf{S}}}
\newcommand{\angleover}{\genfrac{\langle}{\rangle}{0pt}{}}
\newcommand{\biject}{\rightarrowtail\hspace{-8pt}\twoheadrightarrow}
\newcommand{\degree}{^{\circ}}

\newcommand{\asterism}{\[ % putting this in a math block to center it
  \smash{
    \raisebox{-.5ex}{
      \setlength{\tabcolsep}{-.5pt}
      \begin{tabular}{@{}cc@{}}
        \multicolumn2c*\\[-2ex]*&*
      \end{tabular}}}\]}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% change or remove this line to output different or all included tex files
%\includeonly{tex/number-theory}

\begin{document}

\setcounter{secnumdepth}{5}
\setcounter{tocdepth}{1}

% ------------------------------------------------------------------------------

\title{Survey of Mathematical Logic}
\date{draft 2016}
\author{}
\maketitle

% ------------------------------------------------------------------------------

\tableofcontents

\setlength{\parindent}{0pt}
\setlength{\parskip}{1em}
\setlist[itemize]{noitemsep, topsep=0pt}

% ------------------------------------------------------------------------------

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\include{tex/formal-language}
  \include{tex/formal-logic}
  \include{tex/model-theory}
  \include{tex/formal-semantics}

\include{tex/proof-theory}
  \include{tex/recursion-theory}
  \include{tex/type-theory}
  \include{tex/database-theory}

\include{tex/set-theory}
  \include{tex/order-theory}
  \include{tex/graph-theory}
  \include{tex/category-theory}

\include{tex/combinatorics}
  \include{tex/number-theory}
  \include{tex/abstract-algebra}
  \include{tex/linear-algebra}

\include{tex/topology}
  \include{tex/analysis}
  \include{tex/measure-theory}
  \include{tex/probability-theory}

\include{tex/information-theory}
  \include{tex/systems-theory}
  \include{tex/optimization}
  \include{tex/game-theory}

\include{tex/synthetic-geometry}
  \include{tex/algebraic-geometry}
  \include{tex/analytic-geometry}
  \include{tex/fractal-geometry}

\include{tex/appendix}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{thebibliography}{99}

% early bibitems, cites are inline now

\bibitem{hammel03}
    Bill Hammel,
    \emph{Languages, Grammars, Automata \& Quantum Analogs},
    http://graham.main.nc.us/~bhammel/PHYS/autom.html,
    2003

\bibitem{chomsky56}
    Noam Chomsky,
    \emph{Three Models for the Description of Language},
    MIT,
    1956

\bibitem{slonneger-kurtz95}
    Kenneth Slonneger, Barry L. Kurtz,
    \emph{Formal Syntax and Semantics of Programming Languages},
    Addison-Wesley,
    1995

\bibitem{shannon48}
    Claude Shannon,
    \emph{A Mathematical Theory of Communication},
    Bell System Technical Journal,
    1948

\bibitem{turing38}
    Alan Turing,
    \emph{Systems of Logic Based on Ordinals},
    Princeton,
    1938.

\bibitem{kozen97}
    Dexter C. Kozen,
    \emph{Automata and Computability},
    Springer,
    1997

\bibitem{aho69}
    Alfred V. Aho,
    \emph{Nested stack automata},
    Journal of the ACM,
    1969

\bibitem{villemonte02}
    \'Eric Villemonte de la Clergerie,
    \emph{Parsing mildly context-sensitive languages with thread automata},
    COLING '02 Proceedings,
    2002

\bibitem{vijayashanker88}
    K. Vijayashanker,
    \emph{A study of tree adjoining grammars},
    University of Pennsylvania,
    1988

\bibitem{schutzenberger65}
    Mercel-Paul Sch\"utzenberger,
    \emph{On finite monoids having only trivial subgroups},
    Information and Computation,
    1965

\bibitem{mcnaughton-papert71}
    Robert McNaughton, Seymour Papert,
    \emph{Counter-free Automata},
    MIT Press,
    1971

\bibitem{skolem23}
    Thoralf Skolem,
    \emph{The foundations of elementary arithmetic},
    1923,
    trans. Jean van Heijenoort,
    \emph{From Frege to G\"odel: A Source Book in Mathematical Logic, 1879-1931},
    Harvard Univ. Press,
    1967

\bibitem{jaskowski34}
    Stanislaw Ja\'skowski,
    \emph{On the Rules of Suppositions in Formal Logic},
    1934,
    ed. Storrs McCall,
    \emph{Polish logic 1920-39},
    Oxford,
    1967

\bibitem{shapiro00}
    S. Shapiro,
    \emph{Foundations without Foundationalism: A Case for Second-order Logic},
    Oxford University Press,
    2000

\bibitem{prawitz65}
    Dag Prawitz,
    \emph{Natural Deduction: A proof-theoretical study},
    A\&W Stockholm,
    1965

\bibitem{schutte77}
    Kurt Sch\"utte,
    \emph{Proof Theory},
    Springer-Verlag,
    1977

\bibitem{hodges97}
    Wilfred Hodges,
    \emph{A Shorter Model Theory},
    Cambridge University Press,
    1997

\bibitem{birkhoff35}
    Garrett Birkhoff,
    \emph{On the Structure of Abstract Algebras},
    Proceedings of the Cambridge Philosophical Society,
    1935

\bibitem{tarski36}
    Alfred Tarski,
    \emph{Der Wahtheitsbegriff in den formalisierten Sprachen},
    Studia Philosophica,
    1936

\bibitem{ramsey27}
    F.P. Ramsey,
    \emph{Facts and Propositions},
    Aristotelian Society Supplementary Volume 7,
    1927

\bibitem{morley65}
    Michael Morley,
    \emph{Categoricity in Power},
    Transactions of the American Mathematical Society, Vol. 114, No. 2,
    1965

\bibitem{harizanov98}
    Valentina Harizanov,
    \emph{Pure Computable Model Theory},
    Studies in Logic and the Foundations of Mathematics,
    1998

\bibitem{awodey06}
    Steve Awodey,
    \emph{Category Theory},
    Carnegie Mellon,
    2006

\bibitem{maclane69}
    Saunders Mac Lane,
    \emph{Categories for the Working Mathematician},
    Springer,
    1969

\bibitem{boullier94}
    Pierre Boullier,
    \emph{Dynamic Grammars and Semantic Analysis},
    INRIA Research Report No. 2322,
    1994

\bibitem{hott13}
    Univalent Foundations Program,
    \emph{Homotopy Type Theory},
    Institude for Advanced Study,
    2013

\bibitem{lc11}
    Thought Space Zero,
    \emph{Topology},
    \url{https://www.youtube.com/playlist?list=PLF94A6F65866F3F31},
    2011

\bibitem{czoo14}
    MediaWiki,
    \emph{Complexity Zoo},
    \url{https://complexityzoo.uwaterloo.ca},
    2014

\bibitem{corfield08}
    David Corfield,
    \emph{Coalgebraically Thinking},
    \url{https://golem.ph.utexas.edu/category/2011/07/coinductive_definitions.html},
    2008

\bibitem{shulman11}
    Mike Shulman,
    \emph{Coinductive Defenitions},
    \url{https://golem.ph.utexas.edu/category/2011/07/coinductive_definitions.html},
    2011

\bibitem{shulman15}
    Mike Shulman,
    \emph{Introduction to Synthetic Mathematics (Part 1)},
    \url{https://golem.ph.utexas.edu/category/2015/02/introduction_to_synthetic_math.html},
    2015

\bibitem{baez15}
    John Baez,
    \emph{Concepts of Sameness (Part 4)},
    \url{https://golem.ph.utexas.edu/category/2015/02/concepts_of_sameness_part_4.html},
    2015

\bibitem{beall-restall05}
    JC Beall, Greg Restall,
    \emph{Logical Consequence},
    Stanford Encyclopedia of Philosophy,
    2005

\bibitem{hawthorne08}
    James Hawthorne,
    \emph{Inductive Logic},
    Stanford Encyclopedia of Philosophy,
    2008

\bibitem{priest-tanaka-weber13}
    Graham Priest, Koji Tanaka, Zach Weber,
    \emph{Paraconsistent Logic},
    Stanford Encyclopedia of Philosophy,
    2013

\bibitem{laycock10}
    Henry Laycock,
    \emph{Object},
    Stanford Encyclopedia of Philosophy,
    2010

\bibitem{kleene52}
    Stephen Kleene,
    \emph{Introduction to Metamathematics},
    North-Holland Publishing Company,
    1952

\bibitem{ladyman-linnebo-pettigrew11}
    James Ladyman, \/Oystein Linnebo, Richard Pettigrew,
    \emph{Identity and discernibility in philosophy and logic},
    Review of Symbolic Logic, Vol. 5, No. 1,
    2011

\bibitem{curry77}
    Haskell B. Curry,
    \emph{Foundations of Mathematical Logic},
    McGraw-Hill,
    1977

\bibitem{carnap59}
    Rudolph Carnap,
    \emph{The Logical Syntax of Language},
    Littlefield, Adams \& Co.,
    1959

\bibitem{chalmers02}
    David J. Chalmers,
    \emph{On Sense and Intension},
    Blackwell,
    2002

\bibitem{gamut91}
    L. T. F. Gamut,
    \emph{Logic, Language, and Meaning: Introduction to Logic},
    University of Chicago Press,
    1991

\bibitem{goldberg05}
    Mayer Goldberg,
    \emph{On the Recursive Enumerability of Fixed-point Combinators},
    University of Aarhus,
    2005

\bibitem{voevedsky14}
    Vladimir Voevodsky,
    \emph{C-system of a module over a monad on sets},
    http://arxiv.org/abs/1407.3394,
    2014

\bibitem{bastenhof09}
    Arno Bastenhof,
    \emph{Intuitionistic Type Theory and Toposes},
    Seminarium Topos Theorie,
    2009

\bibitem{thompson99}
    Simon Thompson,
    \emph{Type Theory \& Functional Programming},
    University of Kent,
    1999

\bibitem{rondon-kawaguchi-jhala08}
    Patrick M. Rondon, Ming Kawaguchi, Ranjit Jhala,
    \emph{Liquid Types},
    University of California, San Diego,
    2008

\bibitem{martinlof84}
    Per Martin-L\"of,
    \emph{Intuitionistic Type Theory},
    Bibliopolis,
    1984

\bibitem{harper12}
    Robert Harper,
    \emph{Type Theory Foundations},
    Oregon Programming Languages Summer School,
    \url{http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html}
    2012

\bibitem{lemmermeyer-shirali09}
    F. Lemmermeyer, S. Shirali,
    \emph{Group Structure on a Circle},
    Math Gazette, Vol 93 \# 526,
    2009

\bibitem{flajolet-sedgewick09}
    Philippe Flajolet, Robert Sedgewick,
    \emph{Analytic Combinatorics},
    Cambridge University Press,
    2009

\bibitem{seldin03}
    Jonathan P. Seldin,
    \emph{Curry's Anticipation of the Types Used in Programming Languages},
    University of Lethbridge,
    2003

\bibitem{lambek-scott88}
    J. Lambek, P.J. Scott,
    \emph{Introduction to Higher Order Categorical Logic},
    Cambridge University Press,
    1988

\bibitem{jacobs-heunen-hasuo09}
    Bart Jacobs, Chris Heunen, Ichiro Hasuo,
    \emph{Categorical semantics for arrows},
    Journal of Functional Programming,
    2009

\bibitem{wadler14}
    Philip Wadler,
    \emph{Propositions as Types},
    University of Edinburgh,
    2014

\bibitem{rutten00}
    J.J.M.M. Rutten,
    \emph{Universal coalgebra: a theory of systems},
    Theoretical Computer Science 249,
    2000

\bibitem{hatcher02}
    Allen Hatcher,
    \emph{Algebraic Topology},
    Cambridge University Press,
    2002

\bibitem{duponcheel-jones93}
    L. Duponcheel, M.P. Jones,
    \emph{Composing monads},
    Proceedings of the Fifth Annual Glasgow Workshop
      on Functional Programming,
    1993

\bibitem{jones94}
    Mark P. Jones,
    \emph{Qualified types: Theory and practice},
    Cambridge University Press,
    1994

\bibitem{jones95}
    Mark P. Jones,
    \emph{Functional Programming with
      Overloading and Higher-Order Polymorphism},
    Advanced Functional Programming,
    1995

\bibitem{hughes98}
    John Hughes,
    \emph{Generalising Monads to Arrows},
    Science of Computer Programming,
    1998

\bibitem{paterson01}
    Ross Paterson,
    \emph{A New Notation for Arrows},
    ICFP,
    2001

\bibitem{honda-vasconcelos-kubo98}
    Kohei Honda, Vasco T. Vasconcelos, Makoto Kubo,
    \emph{Language primitives and type discipline for structured
      communication-based programming},
    ESOP,
    1998

\bibitem{honda-yoshida-carbone08}
    Kohei Honda, Nobuko Yoshida, Marco Carbone,
    \emph{Multiparty Asynchronous Session Types},
    ACM,
    2008

\bibitem{caires-pfenning10}
    Lu\'is Caires, Frank Pfenning,
    \emph{Session Types as Intuitionistic Linear Propositions},
    CONCUR,
    2010

\bibitem{caires-pfenning-toninho12}
    Bernardo Toninho, Lu\'is Caires, Frank Pfenning,
    \emph{Functions as Session-Typed Processes},
    Springer,
    2012

\bibitem{girard01}
    Jean-Yves Girard,
    \emph{Locus solum: from the rules of logic to the logic of rules},
    Mathematical Structures in Computer Science,
    2001

\bibitem{andreoli92}
    Jean-marc Andreoli,
    \emph{Logic Programming with Focusing Proofs in Linear Logic},
    Journal of Logic and Computation,
    1992

\bibitem{wadler12}
    Philip Wadler,
    \emph{Proposisions as Sessions},
    ICFP '12,
    2012

\bibitem{llwiki16}
    MediaWiki,
    \emph{LLWiki},
    \url{http://llwiki.ens-lyon.fr},
    2016

\bibitem{gay-vasconcelos10}
    Simon J. Gay, Vasco T. Vasconcelos,
    \emph{Linear Type Theory for Asynchronous Session Types},
    Journal of Functional Programming,
    2010

\bibitem{neubauer-thiemann04}
    Matthias Neubauer, Peter Thiemann,
    \emph{An Implementation of Session Types},
    PADL, volume 3057 of LNCS,
    2004

\bibitem{nielson-nielson99}
    Flemming Nielson, Hanne Riis Nielson,
    \emph{Type and Effect Systems},
    ACM Computing Surveys,
    1999

\bibitem{wadler-thiemann03}
    Philip Wadler, Peter Thiemann,
    \emph{The marriage of effects and monads},
    ACM Transactions on Computational Logic,
    2003

\bibitem{filinski99}
    Andrzej Filinski,
    \emph{Representing layered monads},
    26th Symposium on Principles of Programming Languages,
    1999

\bibitem{mcbride13}
    Conor McBride,
    \emph{Ornamental Algebras, Algebraic Ornaments},
    Journal of Functional Programming,
    2013

\bibitem{atkey-mcbride13}
    Robert Atkey, Conor McBride,
    \emph{Productive coprogramming with guarded recursion},
    SICSA,
    2013

\bibitem{plotkin-pretnar08}
    Gordon Plotkin, Matija Pretnar,
    \emph{A Logic for Algebraic Effects},
    23rd Symposium on Logic in Computer Science,
    2008

\bibitem{plotkin-pretnar09}
    Gordon Plotkin, Matija Pretnar,
    \emph{Handlers of Algebraic Effects},
    Programming Languages and Systems, ESOP 2009,
    2009

\bibitem{plotkin-pretnar13}
    Gordon Plotkin, Matija Pretnar,
    \emph{Handling Algebraic Effects},
    Logical Methods in Computer Science 9,
    2013

\bibitem{bauer-pretnar12}
    Andrej Bauer, Matija Pretnar,
    \emph{Programming with Algebraic Effects and Handlers},
    Journal of Logical and Algebraic Methods in Programming,
    2012

\bibitem{pretnar15}
    Matija Pretnar,
    \emph{An Introduction to Algebraic Effects and Handlers},
    ENTCS,
    2015

\bibitem{orchard-yoshida15}
    Dominic Orchard, Nobuko Yoshida,
    \emph{Using session types as an effect system},
    EPTCS,
    2015

\bibitem{orchard-yoshida16}
    Dominic Orchard, Nobuko Yoshida,
    \emph{Effects as Sessions, Sessions as Effects},
    POPL 2016,
    2016

\bibitem{mycroft-orchard-petricek16}
    Alan Mycroft, Dominic Orchard, Tomas Petricek,
    \emph{Effect systems revisited--control-flow algebra and semantics},
    LNCS 9560,
    2016

\bibitem{abramsky-gay-nagarajan96}
    Samson Abramsky, Simon J. Gay, Rajagopal Nagarajan,
    \emph{Interaction Categories and the Foundations of Typed
      Concurrent Programming},
    Deductive Program Design, Marktoberdorf,
    1996

\bibitem{milner-parrow-walker92}
    Robin Milner,
    \emph{A Calculus of Mobile Processes},
    Information and Computation,
    1992

\bibitem{milner92}
    Robin Milner,
    \emph{Functions as processes},
    INRIA,
    1992

\bibitem{jeltsch12}
    Wolfgang Jeltsch,
    \emph{Towards a Common Categorical Semantics for Linear-Time
      Temporal Logic and Functional Reactive Programming},
    MFPS XXVIII,
    2012

\bibitem{jeffrey12}
    Alan Jeffrey,
    \emph{Linear-time Temporal Logic Propositions as Types, Proofs as
      Functional Reactive Programs},
    PLPV'12,
    2012

\bibitem{jeffrey14}
    Alan Jeffrey,
    \emph{Functional Reactive Types},
    LICS'14,
    2014

\bibitem{hyland-power06}
    Martin Hyland, John Power,
    \emph{Discrete Lawvere theories and computational effects},
    TCS,
    2006

\bibitem{haghverdi-scott05}
    Esfandiar Haghverdi, Philip Scott,
    \emph{Towards a Typed Geometry of Interaction},
    Proc. Computer Science Logic,
    2005

\bibitem{winskel-nielsen93}
    Glynn Winskel, Mogens Nielsen,
    \emph{Models for concurrency},
    Aarhus University,
    1993

\bibitem{aczel88}
    Peter Aczel,
    \emph{Non-well-founded sets},
    CSLI,
    1988

\bibitem{selinger01}
    Peter Selinger,
    \emph{Control Categories and Duality: on the Categorical Semantics
    of the Lambda-Mu Calculus},
    Mathematical Structures in Computer Science,
    2001

\end{thebibliography}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%