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? Cheers, -- Artur Oliveira Gomes
example-06-05.doc
Description: MS-Word document
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
