[ProofPower] Rewriting from assumptions - parenthesis problem

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

Re: [ProofPower] Rewriting from assumptions - parenthesis problem

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)) (* |- *) \exist