Jon, 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 proof. Again, make sure you rewrite with everything you need to use. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
