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