\begin{zed}
  State \defs [x:\num | x < 10] \\
  Init  \defs [State | x=0] \\
  Incr  \defs [\Delta State | x' = x+1 ] \\
  Decr  \defs [\Delta State | x' = x-1 ] \\
  Jump  \defs [\Delta State; d?:\nat | x' = x+d? ] \\
  Show  \defs [\Xi State; v!:\num | v! = x ]
\end{zed}

  We can use Z/EVES as a simple animator, by using \textbf{try} to
  evaluate/simplify schema expressions like:

\begin{zed}
  Test1 \defs Init' \semi Incr \semi Decr \semi Incr \\
  Test2 \defs Init' \semi Jump[d? := 3] \\
\end{zed}

  If we ask Z/EVES to evaluate $Test1$, then it will
  simplify this sequence of operation schema as much as possible,
  hopefully down to something that just tells us the final
  output/state values. 

try Test1;
prove by reduce;

  For this simple example, Z/EVES would come back with:

\begin{zed}
x' = 1
\end{zed}

  We do not have to start from the $Init$ operation.
  Instead, we might define some interesting intermediate state,
  then call operations starting from that state. 

\begin{zed}
  StateA \defs [State | x = 8] \\
  Test3  \defs StateA' \semi Incr \\
  Test4  \defs StateA' \semi Incr \semi Incr
\end{zed}

  Can you guess what $Test4$ will produce?

  By the way, if several operation schema have an output variable with 
  the same name, you need to rename them to be unique.  Otherwise,
  the two outputs will have the same name so will be required to
  have the same value.

\begin{zed}
  Test5  \defs StateA' \semi Show \semi Incr \semi Show \\
  Test6  \defs StateA' \semi Show \semi Incr \semi Show[v2!/v!] \\
\end{zed}