\include{prelude}

\begin{document}

\frontmatter
\pagenumbering{roman}
\setcounter{page}{1}

\thispagestyle{empty}

{\begingroup
\vspace*{0.08\textheight}
\ifdefined\TABLET
  \def\titlemargin{0.2\textwidth}
\else
  \def\titlemargin{0.3\textwidth}
\fi
\noindent
\hspace*{\titlemargin}{\Large\strut Anne Baanen} \\[.5\jot]
\noindent
\hspace*{\titlemargin}{\Large\strut Alexander Bentkamp} \\[.5\jot]
\noindent
\hspace*{\titlemargin}{\Large\strut Jasmin Blanchette} \\[.5\jot]
\noindent
\hspace*{\titlemargin}{\Large\strut Johannes H\"olzl} \\[.5\jot]
\noindent
\hspace*{\titlemargin}{\Large\strut Jannis Limperg} \\[0.16\textheight]
\noindent
\hspace*{\titlemargin}{\Huge\bfseries\itshape The Hitchhiker's Guide to\strut}\par
{\raggedleft\Huge\bfseries\itshape Logical Verification\strut\par}
\bigskip
\bigskip
\noindent
\hspace*{\titlemargin}{\Large\bfseries\itshape 2025\
\ifdefined\LMU
  LMU
\else
\fi
\edition{}~Edition} \\[\jot]
\noindent
\hspace*{\titlemargin}{(\today)}
\vfill
\noindent
\hspace*{\titlemargin}{\includegraphics[width=0.1\textwidth]{images/lfwd_icon_black}\par\medskip}
\noindent
\ifdefined\LMU
  \hspace*{\titlemargin}{\Large
  \href{https://www.tcs.ifi.lmu.de/lehre/ss-2025/itp_de.html}{www.tcs.ifi.lmu.de/}\par}
  {\raggedleft\Large
  \href{https://www.tcs.ifi.lmu.de/lehre/ss-2025/itp_de.html}{lehre/ss-2025/itp\_de.html}\hspace*{0.0225\textwidth}\par}
\else
  \hspace*{\titlemargin}{\Large
  \href{https://lean-forward.github.io/hitchhikers-guide/2025}{lean-forward.github.io/}\par}
  {\raggedleft\Large
  \href{https://lean-forward.github.io/hitchhikers-guide/2025}{hitchhikers-guide/2025}\hspace*{0.0225\textwidth}\par}
\fi
\vspace*{0.08\textheight}
\endgroup}

\newpage

~

\vfill

{\raggedright
\noindent
Copyright \copyright{} 2018--2025 Anne Baanen, Alexander Bentkamp, Jasmin
Blanchette,
Johannes H\"olzl, and Jannis Limperg. All rights reserved.

}

\newpage

\pagestyle{plain}
\setcounter{tocdepth}{1}

\tableofcontents

\include{preface}

\thispagestyle{plain}
\pagestyle{loveheadings}

\mainmatter
\pagenumbering{arabic}
\setcounter{page}{1}

\part{Basics}

\include{ch01-types-and-terms}
\include{ch02-programs-and-theorems}
\include{ch03-backward-proofs}
\include{ch04-forward-proofs}

\part{Functional--Logic Programming}

\include{ch05-functional-programming}
\include{ch06-inductive-predicates}
\include{ch07-effectful-programming}
\include{ch08-metaprogramming}

\part{Program Semantics}

\include{ch09-operational-semantics}
\include{ch10-hoare-logic}
\include{ch11-denotational-semantics}

\part{Mathematics}

\include{ch12-logical-foundations-of-mathematics}
\include{ch13-basic-mathematical-structures}
\include{ch14-rational-and-real-numbers}

\raggedright

\bibliography{bib}{}
\bibliographystyle{abbrv}

\end{document}
