Hi there,

I am trying to calculate preconditions of operations in Z using ProofPower.
But after strip and rewriting, I can not be able to current goal. (see
attached file)
I am not pretty sure of which steps should I take to achieve the goal.
Maybe I am not using the correct witnesses in the z_E_tac, in the
beginning of the proof.

Could someone guide me through this please?


Artur Oliveira Gomes

Attachment: example-06-05.doc
Description: MS-Word document

Proofpower mailing list

Reply via email to