[CST-2] Spec Ver I - 1997/7/1

[Matej Pfajfar]

> >   |- { P /\ (1 <= v) /\ (v <= e) } S { P[v+1/v] }
> > --------------------------------------------------- (REPEAT)
> > |- { P[1/v] /\ (E = e) /\ (1 <= e) } S { P[e+1/v] }
> >
> > We do not need any side conditions.
> >
> > Any thoughts?
Forgot to say - the specification that you need to prove is that Y >= 0,
in contrast to the assumption at the beginning of the question, that e >
0. So you probably need to modify this so it can work with E=0.

Matej Pfajfar
St John's College, University of Cambridge, UK

GPG Public Key @ http://matejpfajfar.co.uk/keys
Most people are good people, the rest of us are going to
run the world. -- badbytes

WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
         15/07/2002. PLEASE USE mp@cantab.net.