On 15 May 2009, at 04:49, Artur Oliveira Gomes wrote:

Hi there,

I am having a problem in rewriting using an assumption with parenthesis.
For example:
(* 1 *) (\exists (SA AND SB)' · SAInit AND SBInit)
= ((\exists SA' · SAInit) AND (\exists SB' · SBInit))
(* |- *) \exists (SA AND SB)' · SAInit AND SBInit

The rewriting does not occur due to the parenthesis in the LHS.
Does anyone know what should I do to solve this problem?

It doesn't look like parentheses are the problem. It might be a problem with types or something else that is not visible in the pretty- printed Z that is stopping the LHS of he assumption matching the conclusion of the goal. Can you provide an example with definitions of SA etc. that can be run?

Regards,

Rob



Cheers,

--
Artur Oliveira Gomes
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to