I noticed that you were writing
rewrite_tac [z_get_spec %SZT% pre Op %>%]
to rewrite the pre operator away. In some cases this would leave Op in
the result which you would then need to rewrite away again. It's
probably better to just do
rewrite_tac [z_get_spec %SZT% Op %>%]
and let the z_li
My first response to Artur Gomes was a bit rushed
and probably didn't help much, so I had another
look.
I fiddled around with his script to confirm that
the precondition of Op is SS, and then did
a direct proof.
The amended script is attached.
I don't have a systematic method to offer, not having
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 precondi
Hi there,
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.
Here follows an attached file with a small example o
