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
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.
Proofpower mailing list