\documentclass[a4paper]{scrartcl}

\usepackage[backend=biber,natbib]{biblatex}
\bibliography{library}

\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\renewcommand{\qedsymbol}{$\blacksquare$}
\let\leq\leqslant
\let\le\leqslant
\let\geq\geqslant
\let\ge\geqslant
% See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of
% definitions and examples.
\newtheoremstyle{mydefinition}%
	{2em}{2em}% Space above and below
	{}% Body font
	{}% Indent
	{\bfseries}% Theorem head font
	{}% Punctuation after theorem head
	{0pt}% Space after theorem head
	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
\theoremstyle{mydefinition}
\newtheorem{xdefinition}{Definition}
\newenvironment{definition}%
	{\pushQED{\qed}\begin{xdefinition}}%
	{\popQED\end{xdefinition}}
\newtheoremstyle{myexample}%
	{2em}{2em}% Space above and below
	{}% Body font
	{}% Indent
	{\itshape}% Theorem head font
	{}% Punctuation after theorem head
	{0pt}% Space after theorem head
	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
\theoremstyle{myexample}
\newtheorem{xexample}{Example}
\newenvironment{example}%
	{\pushQED{\qed}\begin{xexample}}%
	{\popQED\end{xexample}}
\newtheorem{xremark}{Remark}
\newenvironment{remark}%
	{\pushQED{\qed}\begin{xremark}}%
	{\popQED\end{xremark}}
\newtheoremstyle{exercise}{1em}{1em}{}{}{\scshape}{.}{1em}{}
\theoremstyle{exercise}
\newtheorem{exercise}{Exercise}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{relsize}
\usepackage{parskip}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{stackengine}
\crefname{figure}{Figure}{Figures}
\usepackage[color]{changebar}
\newif\ifchangebar\changebarfalse
\let\oldcbend\cbend
\def\cbend{\oldcbend\changebarfalse}
\newcommand{\erin}{\ifchangebar\cbend\fi\cbcolor{yellow}\cbstart\changebartrue}
\newcommand{\camil}{\ifchangebar\cbend\fi\cbcolor{red}\cbstart\changebartrue}

\renewcommand*{\arraystretch}{1.3}

\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
\DeclareMathOperator{\Uop}{\mathbf{U}}
\DeclareMathOperator{\Wop}{\mathbf{W}}
\DeclareMathOperator{\Xop}{\bigcirc}
\DeclareMathOperator{\Fop}{\lozenge}
\DeclareMathOperator{\Gop}{\square}
\DeclareMathOperator{\Sop}{\mathbf{S}}
\DeclareMathOperator{\Pop}{\bigcirc^{--1}}

\title{Model Checking}
\subtitle{Assignment 1}
\author{Camil Staps \and Erin van der Veen}

\begin{document}

\maketitle

\setcounter{section}{5}
\setcounter{subsection}{2}

\input{intro}
\input{syntax}
\input{semantics}
\input{specifying-properties}
\input{equivalence}
\input{conversion}
%TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper
\input{bad-prefix}

\input{summary}
\input{bibliographic-notes}
\input{exercises}

\printbibliography

\section*{Contribution}
%TODO: Like we are some immature group of children, we have to provide proof of contribution
\camil
Erin has started writing the text.
This text was then copy-edited, slightly corrected where needed and expanded by Camil.
(The result was then copy-edited, slightly corrected where needed and expanded by Erin.
The result was then copy-edited, slightly corrected where needed and expanded by Camil.)$^\omega$
In the above, yellow bars indicate content primarily contributed by Erin, whereas red bars indicate content primarily contributed by Camil.
Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend

\end{document}