On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote: >I'm having hard times to achieve some proofs of preciondition >and initialization using ProofPower. >The file attached contains 3 examples that I still can not prove. >If anyone could help me out with those proofs, I will be thankful.
These are all existential conjectures. ProofPower is sometimes quite dumb about these things (sometimes quite smart), it only really knows about the kinds of existential proofs which are necessary for proving consistency of things like recursive definitions (and that stuff only really works for HOL its not so good in Z). So usually you will have to come up with a witness for the existential goal yourself. In the case of an existential with a schema as the signature the witness will usually be a binding display. So for each of your proofs you must come up with the binding display of a witness for your conjecture, i.e. a binding which satisfies the body of the existential, and then offer it up using exists-tac. Then you have to prove that your witness does satisfy the predicate. (I didn't check whether you are trying to prove the right thing!) regards, Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
