\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}
\tikzset{>=stealth}
\tikzset{state/.append style={minimum size=15pt}}
\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}{\raisebox{1pt}{$\bigcirc$}}
\DeclareMathOperator{\Fop}{\lozenge}
\DeclareMathOperator{\Gop}{\square}
\DeclareMathOperator{\Sop}{\mathbf{S}}
\DeclareMathOperator{\Pop}{\raisebox{1pt}{$\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{Past Modalities in LTL}
\subtitle{Model Checking, Assignment 1}
\author{Camil Staps \and Erin van der Veen}

\begin{document}

\both
\maketitle

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

% The extra newlines are needed for correct changebars

\input{intro}

\input{syntax}

\input{semantics}

\input{equivalence}

\input{conversion}

\input{bad-prefix}

\input{summary}

\input{exercises}

\both
\printbibliography

\section*{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, shortcomings of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process.
\cbend

\end{document}