
\section{\label{sec:sensible_unnamed_patch_sequences}Sensible Unnamed Patch Sequences}

\begin{Idefinition}[sensible-sequences]
We classify some unnamed patch sequences as \emph{sensible}.

\begin{Iexplanation}
For example, the sequence `add file foo; insert ``hello world'' into
foo' is sensible, whereas `insert ``hello world'' into foo' is not
sensible, as it doesn't make sense to insert text into a file without
first adding the file.
\end{Iexplanation}
\end{Idefinition}

\start{axiom}{doing-nothing-is-sensible}
$\nopatches$ is sensible.
\begin{Iexplanation}
If you haven't done anything then you certainly haven't done anything
that isn't sensible.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{sensible-subsequences}
If $\unnamed{\seq{p}} \unnamed{q}$ is sensible then $\unnamed{\seq{p}}$
is sensible.
\begin{Iexplanation}
If you are doing sensible things, then you can stop at any time, and the
rseult will be sensible.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{commute-preserves-sensibility}
If $\unnamed{\seq{p}} \unnamed{q} \unnamed{r} \unnamed{\seq{s}}$ is
sensible and
$\pair{\unnamed{q}}{\unnamed{r}} <-> \pair{\unnamed{r'}}{\unnamed{q'}}$,
then $\unnamed{\seq{p}} \unnamed{r'} \unnamed{q'} \unnamed{\seq{s}}$ is
sensible.
\begin{Iexplanation}
Commuting patches maintains sensibility.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{sensible-inverse}
If $\unnamed{\seq{p}} \unnamed{\seq{q}}$ is sensible then
$\unnamed{\seq{p}} \unnamed{\seq{q}} \unnamed{\seq{q}}^$ is
sensible.
\begin{Iexplanation}
Undoing patches takes us back to an earlier sensible situation.
\end{Iexplanation}
\end{Iaxiom}

