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_library proof context simplify
pre [... | ...]
automatically.
Phil
Artur Oliveira Gomes wrote:
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 of what I am trying
to do.
Best regards,
--
Artur Oliveira Gomes
------------------------------------------------------------------------
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
The information contained in this E-Mail and any subsequent
correspondence is private and is intended solely for the intended
recipient(s). The information in this communication may be
confidential and/or legally privileged. Nothing in this e-mail is
intended to conclude a contract on behalf of QinetiQ or make QinetiQ
subject to any other legally binding commitments, unless the e-mail
contains an express statement to the contrary or incorporates a formal Purchase Order.
For those other than the recipient any disclosure, copying,
distribution, or any action taken or omitted to be taken in reliance
on such information is prohibited and may be unlawful.
Emails and other electronic communication with QinetiQ may be
monitored and recorded for business purposes including security, audit
and archival purposes. Any response to this email indicates consent
to this.
Telephone calls to QinetiQ may be monitored or recorded for quality
control, security and other business purposes.
QinetiQ Limited
Registered in England & Wales: Company Number:3796233
Registered office: 85 Buckingham Gate, London SW1E 6PD, United Kingdom
Trading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom
http://www.qinetiq.com/home/notices/legal.html
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
