%% This file was automatically generated by preproc.
%  Copyright (C) 2007 David Roundy
%
%  This program is free software; you can redistribute it and/or modify
%  it under the terms of the GNU General Public License as published by
%  the Free Software Foundation; either version 2, or (at your option)
%  any later version.
%
%  This program is distributed in the hope that it will be useful,
%  but WITHOUT ANY WARRANTY; without even the implied warranty of
%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%  GNU General Public License for more details.
%
%  You should have received a copy of the GNU General Public License
%  along with this program; see the file COPYING.  If not, write to
%  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
%  Boston, MA 02110-1301, USA.

\documentclass{article}
%\usepackage{color}

\usepackage{verbatim}
\newcommand{\htmladdnormallink}[2]{#1}
\newcommand{\htmladdnormallinkfoot}[2]{#1\footnotetext{\tt #2}}
\usepackage{fancyvrb}
\newenvironment{code}{\comment}{\endcomment}
% \newenvironment{code}{\color{blue}\verbatim}{\endverbatim}

\newcommand{\commutes}{\longleftrightarrow}

\begin{document}


\section{Patch properties}

Darcs is built on a hierarchy of patch types.  At the lowest level are
``primitive'' patches, and from these building blocks, a whole hierarchy of
patch types are built.  Each of these patch types must support a number of
functions, which must obey a number of laws.

\subsection{Properties of identity}

\newtheorem{prp}{Property}

\begin{prp}[Identity commutes trivially]
  The identity patch must commute with any patch without modifying said patch.
\end{prp}


\begin{prp}[Inverse doesn't commute]
  A patch and its inverse will always commute, unless that patch is an
  identity patch (or an identity-like patch that has no effect).
\end{prp}


\subsection{Commute properties}

\begin{prp}[Recommute]
  $AB \commutes B'A'$ if and only if $B'A' \commutes AB$
\end{prp}


\begin{prp}[Commute inverses]
  $AB \commutes B'A'$ if and only if $B^{-1}A^{-1} \commutes A'^{-1}B'^{-1}$
\end{prp}


\begin{prp}[Patch and inverse]
  If $AB \commutes B'A'$ then $A^{-1}B' \commutes BA'^{-1}$
\end{prp}

This property is only true of primitive patches.


\begin{prp}[Permutivity]
  (to be added...)
\end{prp}


\end{document}