Got that error corrected, thanks for the input. Encounterd a few more hang
ups on doing the proof but those were eliminated by grabbing the spec for
elevator on the rewrite tactic. Same for floor.

Now I am back to the Init operations. I have attached the specification
again for you veiwing, but if I remember correctly we were going with using
the "There Exists" proof still on these like we did for the States.

Any direction on how to finish these up so I may move on to the actual
operations would be greatly appreciated.


On Sat, Oct 13, 2012 at 12:28 PM, Roger Bishop Jones <>wrote:

> 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

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to