On Sunday 14 Oct 2012 04:52, you wrote:

> Any direction on how to finish these up so I may move on
> to the actual operations would be greatly appreciated.

Two points to keep in mind.

First, ProofPower does not automatically rewrite with any of 
the specifications which you have put in, you have to tell it 
which you want it to rewrite with, and in your remaining 
precondition proofs there are more specifications which you 
have to include in the rewrite.
It is possible to make a proof context which expands the 
default set of rewrites, but at this stage you are probably 
better just using cut and paste on the lists of global 
variable names used in the rewrites.

Second, when proving the non-emptyness of a schema, as in 
the initial conditions, you have to think of the schema as a 
set of bindings, consider the conditions which you have 
placed on which bindings belong to the schema, and then 
think of a way of writing down a binding which can be proven 
to satisfy the conditions.
That will be your witness, then you just have to do the 
Again, make sure you rewrite with everything you need to 


Proofpower mailing list

Reply via email to