\section{Conclusion}
We have provided an operational model for Dunne's abstract commands
and their operators, except that our model does not provide any information
about the frame of a command.
Based upon this model, we have been able to prove,
using the automated prover Isabelle, 
Dunne's definitions of the abstract command operators, except their frames.
That is, we have shown that they follow from our operational model
--- equivalently, that our commands defined operationally satisfy the 
definitions given by Dunne.

We have discussed the problems in including the frame of a command in
this work.
Briefly, while the frame of a command might be thought of as the set
of variables which ``might'' be set by the command, commands such as
$x := x$ (whose frame is $\{x\}$) prevent us from defining the command's
frame from its behaviour.
We could have tried to show that the frame of a command
(as defined by Dunne) conforms to a rule that the frame contains
any variable which can be changed by the command, but this 
generally seems obvious.

Formalising the various definitions for use in the mechanised
prover has highlighted aspects of the specification of commands 
which need to be considered, but are easily overlooked until one
formalises them.  Examples of this appear in our discussions about 
``syntactic'' and ``semantic'' expressions and commands, about
the language used to form ``syntactic'' expressions,
and about the meaning of quantifying over a set $x$ of program variables.

\subsubsection{Acknowledgement.} 
We wish to thank Steve Dunne for his very great assistance in 
some lengthy discussions on the topic.