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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
