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 >> >

**
errorEncountered.doc.gz**

*Description:* GNU Zip compressed data

**
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