Roger,

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.

Regards,
Jon


On Mon, Nov 5, 2012 at 9:20 AM, Jon Lockhart <jal...@bucknell.edu> 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" <r...@rbjones.com> 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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to