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.

Roger Jones

Proofpower mailing list

Reply via email to