That linear arithmetic command worked great and finished off the solution
no problem. Unfortunately I realized I needed to show that the starting and
calling floors were greater than zero not greater than or equal to zero. I
have modified my goal as such, and was able to prove the first sub goal.
The third sub goal should be easy to get since it is exactly like what I
was originally proving. I am having trouble though with the second goal,
which the point I am at can be seen in the error encountered document I
have provided.

It looks exactly like goal one, but the linear arithmetic tactic fails to
solve it, and I tired introducing a lemma through LEMMA_T, since I could
not get lemma_tac working, and I would believe that should give the system
enough to prove the goal, but apparently not. It logically makes since in
my head.


On Mon, Nov 5, 2012 at 9:20 AM, Jon Lockhart <> wrote:

> Roger,
> Thank you very much. I will take a look a this tactic.
> Regards,
> Jon
> On Nov 5, 2012 4:27 AM, "Roger Bishop Jones" <> wrote:
>> Jon,
>> I should have mentioned that the problem goal you are
>> looking at can be solved by linear arithmetic so you don't
>> need any lemma at all.
>> Linear arithmetic is not covered by the tutorlal but this is
>> one way to prove the goal:
>> a (PC_T1 "z_lin_arith" asm_prove_tac[]);
>> Roger

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

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

Proofpower mailing list

Reply via email to