Jon, On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote:
> I am having a little trouble getting the axioms created, > moving the static portions of the Button_State to an > axiom from the schema. I can't seem to get the proof to > operate properly. Any suggestions? The problem is that the existential goal you are trying to prove has decorations on the names of the variables, but the witness you have supplied does not. This is a point of difference between proving the non- emptyness of a schema and the consistency of an axiomatic specification. Because the names in the signature of the axiomatic spec have already been introduced as global variables (aka constants), they cannot be used as the names in the existential which must be proven to establish the consistency of the axiomatic specification. So they get primed. When z exists tac complains that it can't match the witness against the signature of the existential, first check that the names you have used in the binding are exactly those in the existential you are trying to prove, then check that the expressions have the right type. regards, Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
