\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}
\newtheoremstyle{theorem}%
	{1em}{1em}%
	{\itshape}%
	{}%
	{\itshape\bfseries}%
	{}%
	{0pt}%
	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}
\theoremstyle{theorem}
\newtheorem{theorem}{Theorem}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{relsize}
\usepackage{parskip}
\usepackage{cleveref}
\usepackage{enumitem}
\usepackage{multicol}
\usepackage{stackengine}
\crefname{figure}{Figure}{Figures}
\crefname{xdefinition}{Definition}{Definitions}
\crefname{xexample}{Example}{Examples}
\crefname{xremark}{Remark}{Remarks}
\crefname{exercise}{Exercise}{Exercises}
\crefname{algorithm}{Algorithm}{Algorithms}
\usepackage[color]{changebar}
\newif\ifchangebar\changebarfalse
\let\oldcbend\cbend
\def\cbend{\oldcbend\changebarfalse}
\newcommand{\changechangebar}[2][2pt]{\ifchangebar\cbend\fi\cbcolor{#2}\cbstart[#1]\changebartrue}
\newcommand{\erin}{\changechangebar{yellow}}
\newcommand{\camil}{\changechangebar{red}}
\newcommand{\both}{\changechangebar[1pt]{orange}}

\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}}

\newcommand{\wff}{\emph{wff}} % Well-formed formula
\newcommand{\wffn}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{0}}} % Pure present wff
\newcommand{\wfff}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$+$}}} % Pure future wff
\newcommand{\wffp}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{$-$}}} % Pure past wff

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

\begin{document}

\both
\maketitle

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

\input{intro}
\input{syntax}
\input{semantics}
\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}

\both
\printbibliography

\section*{Contribution}
%TODO: Like we are some immature group of children, we have to provide proof of contribution
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.
Thin orange bars indicate material that cannot be attributed to either.
Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend

\end{document}