# Rewrite rules don't rewrite this equality.

```Dear volunteers,

I'm trying to prove a theorem in which I compute a result inside
an if, and then add that result to something else. PVS revision
2.408, on a regular Sun running Solaris. Here's my test theory:

%%%
test : THEORY
BEGIN
struct : TYPE = [# ins:nat, outs:nat #]

f(a:struct) : nat = outs(a) ;

alemma : LEMMA
(forall (a:struct) :
(if ins(a)>0 then f(a) else outs(a) endif)=outs(a)
)

dilemma : THEOREM
(forall (a:struct, b:struct) :
(if ins(a)>0 then f(a) else outs(a) endif)+
(if ins(b)>0 then f(b) else outs(b) endif)=
outs(a)+outs(b)
)
END test
%%%

The idea is that I can apply alemma twice with different
instantiations (ie. a<-a!1, a<-b!1) to prove dilemma.

%%%
(skolem!)(lemma "alemma" ("a" "a!1"))(lemma "alemma" ("a" "b!1"))
%%%

However, once I've done that, I end up with this:

%%%
dilemma :

[-1]    (IF ins(b!1) > 0 THEN f(b!1) ELSE outs(b!1) ENDIF) = outs(b!1)
[-2]    (IF ins(a!1) > 0 THEN f(a!1) ELSE outs(a!1) ENDIF) = outs(a!1)
|-------
[1]    (IF ins(a!1) > 0 THEN f(a!1) ELSE outs(a!1) ENDIF)
+ (IF ins(b!1) > 0 THEN f(b!1) ELSE outs(b!1) ENDIF)
= outs(a!1) + outs(b!1)

Rule? (assert)
No change on: (ASSERT)
dilemma :
%%%

It seems to me that not enough is being rewritten here; running
(grind) rewrites the f() calls and then simplifies, which doesn't
work for the theory I'm really interested in, since it's more
complicated. Am I missing some prover command to do this,
or what? My thanks for your help,