Artur, On Thursday 20 August 2009 15:02:55 Artur Oliveira Gomes wrote:
>I am having few problems with the precondition calculus. More specifcly, >I can not say if an existential quantifier included in the predicate of the >operation >can be eliminated during the calculus, or if it is the precondition itself. I think this will work out better if you use (at least initially) the proof context z_library_ext, which will bring you down to an existential goal on the first rewrite. Its not possible to use exists tac unless the existential is at the top level. (Perhaps you were doing that, but its not in your script). However, if you proceed as if you were trying to prove the goals you state, you will of course fail, since the goal is false. Your script looks as if you are doing that. Starting with the "pre Op = true" goal, is just a way of simplifying the precondition as a prelude to actually proving the simplification with a goal like "pre Op <=> expression" or "pre Op = [ | ]". regards, Roger Jones _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
