I've decided that I want to implement the Set machine in terms of a Seq machine with the following interface:
I'm going to define the actions such that
the state where 
is unreachable.
You'll see why soon.
Seq = (
see above 
see next page 
).
Seq's actions have the following specification:
1
addh (i: int)/ok()pre
post
remh()/ok(int)
pre
post
size()/ok(int)
pre true
post
isin(i: int)/ok(bool)
pre true
post
fetch(i: int)/ok(int)
pre
post
