\documentclass{article}
\usepackage{z-eves}
\parindent 0pt          % Don't indent the first line of each paragraph.
\parskip 1ex plus 3pt   % Leave about half a blank line between paragraphs.
\begin{document}

\section{Testing the Add Operation}


\subsection{TTF Tree for Add}

[ Note how I use spaces for indentation (to indicate the tree depth)
  I've chosen to put strategy names in [...] brackets.
  Each strategy name is then explained and justified later.
  All the non-bracketed names are schema names and these are
  also given later.

  The begin..end verbatim makes LaTeX reproduce this exactly
  as I've typed it, with the given indentation.
]

\begin{verbatim}
AddVIS
    [ZeroOneMany]
    AddZero

    AddOne
        [CauseEffect]
        AddOneA

        AddOneB

    AddMany
        [CauseEffect]
        AddManyA

        AddManyB

        AddManyC
\end{verbatim}


\subsection{Rationale for Add Tests}

The main schema for the whole $SGSAdd$ operation is
(simplifying $pre~SGSAdd$):

\begin{schema}{AddVIS}
  stu : Grade \fun IDSet \\
  g?  : Grade \\
  i?  : ID
\where
  (\forall a,b:Grade @ a \neq b \implies \\
  \t1  (stu~a).s \cap (stu~b).s = \emptyset)
\end{schema}

Starting from this schema, I applied the [ZeroOneMany]
strategy, because ... [it is not necessarily a good choice].
This produces the following three schemas:

\begin{schema}{AddZero}
  ...
\end{schema}

\begin{schema}{AddOne}
  ...
\end{schema}

\begin{schema}{AddMany}
  ...
\end{schema}

The $AddZero$ schema does not need further expansion.

For the $AddOne$ schema, I decided to use the
[CauseEffect] strategy, because in this case ...
This produces the following schemas:

\begin{schema}{AddOneA}
  ...
\end{schema}

\begin{schema}{AddOneB}
  ...
\end{schema}

For the $AddMany$ schema, I decided to use the
[CauseEffect] strategy again, because ...
This produces the following schemas:

\begin{schema}{AddManyA}
  ...
\end{schema}

\begin{schema}{AddManyB}
  ...
\end{schema}

\begin{schema}{AddManyC}
  ...
\end{schema}

\end{document}