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