[CST-2] Spec&Ver I

[Matt Williams]

> > > > > I think it's clearer just to say (X=0 n 0=1) is clearly
> > > > > false, and since F => anything, then choose the anything to
> > > > > be 0=0, and by precondition strengthening you then get the
> > > > > assignment axiom.

That's a good point.

> > > > But then that's not technically following the rules of the system...
> > >
> > > Yes it is:
> > >  X=0 n 0=1 => X=0 n F => F
> > >
> > > I'm sure you can do that?
> >
> > Ok then if you use precondition strengthening lots of times.

I think you should only need to use pre-condition strengthening once since
A => B => C means that A => C.

> Hehe.. if you feel like writing everyone of them out, I suspect you
> can shortcut stuff like this fine and he won't mind.

Yeah, I suspect he wouldn't mind.

Matt