# Re: [ProofPower] Rewriting from assumptions - parenthesis problem

```
On 18 May 2009, at 21:28, Artur Oliveira Gomes wrote:```
```
```
```Hi there,

```
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?
```
Yes, an example is attached here as follows.

```
```
```
I see the problem now. Remember that the quantifier symbols in Z are used for two different language constructs: predicates and schemas. Because you used = rather than %equiv% in your lemma, the lemma proves an equation between schemas and the left-hand side doesn't match the conclusion of the goal (which is a predicate). The easiest thing to do is to change = to %equiv%, which makes the lemma into a logical equivalence between predicates rather than an equation between schemas. This makes the proof of the lemma a bit simpler too, although it does require a little trick to avoid the lemma causing a case split:
```
set_goal ([],%SZT%%exists% (AState %and% BState %and% CState)'
%spot% InitAState %and% InitBState %and% InitCState%>%);

```
(* lemma says conclusion %equiv% conclusion': use LEMMA_T ... rewrite_thm_tac to avoid case split *)
```
a (LEMMA_T %SZT%(%exists% (AState %and% BState %and% CState)'
%spot% InitAState %and% InitBState %and% InitCState)
%equiv% ((%exists% AState'%spot% InitAState)
%and% (%exists% BState'%spot% InitBState)
%and% (%exists% CState'%spot% InitCState))%>%
rewrite_thm_tac);
(* *** Goal "1" *** *)
a (REPEAT strip_tac);
(* *** Goal "1.1" *** *)
a(z_%exists%_tac %SZT%%theta%(AState')%>% THEN asm_rewrite_tac[]);
(* *** Goal "1.2" *** *)
a(z_%exists%_tac %SZT%%theta%(BState')%>% THEN asm_rewrite_tac[]);
(* *** Goal "1.3" *** *)
a(z_%exists%_tac %SZT%%theta%(CState')%>% THEN asm_rewrite_tac[]);
(* *** Goal "1.4" *** *)
```
a(z_%exists%_tac %SZT%%theta%((AState %and% BState %and% CState)')%>% THEN asm_rewrite_tac[]);
```
(* Lemma now proved and have new rewritten conclusion to prove ... *)

Regards,

Rob.

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