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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
