On Friday 12 Oct 2012 20:35, Jon Lockhart wrote:
> I got back to the specification today, and moved on to
> proving the elevator state schema, Elevator_State, and I
> moved the static component elevator to an axiom, similar
> to the static components of button. Unfortunately I get
> a weird sub goal pop up that says "{} = elevator" after
> I work on the existence proof. Is this b/c I used the
> empty set as the witness to the elevator axiom proof?

No, its because you set both moving and stopped to the empty 
set, and this can only be the case if there are no 
Your spec doesn't say there are no elevators, so you can't 
prove it.

You need to supply a witness for which the union of "moving" 
and "stopped" can be proven to be "elevators", even though 
you don't know what "elevators" is.
One way to do that is to use the state in which everything 
is stopped, i.e. in which moving = {} and stopped = 

I haven't checked that that satisfies the rest of the 
predicate, but I guess that's probable.


Proofpower mailing list

Reply via email to