[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] rewrites and forall_or

I am working with a formula of the form
 ...
|-------
[1] (FORALL (x) : (A OR (B OR C)))

I use the rewrite step with the "forall_or" lemma from the prelude and
get 

 ...
|-------
[1] (FORALL (x) : A) OR (FORALL (x) :  (B OR C)) 

I apply it again and get 

 ...
|-------
[1] (FORALL (x) : B) OR (FORALL (x) : C)
[2] (FORALL (x) : A) OR (FORALL (x) : (B OR C))

What I want to get is 

 ...
|-------
(FORALL (x) : A) OR (FORALL (x) : B) OR (FORALL (x) : C)

Is this possible using built-in strategies and the forall_or lemma or
a lemma similar to it? 

Thanks, 

    Erika