Jon, 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 elevators. 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 = elevators. I haven't checked that that satisfies the rest of the predicate, but I guess that's probable. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com