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
>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 = [ | ]".

Roger Jones

Proofpower mailing list

Reply via email to