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

[PVS-Help] Existentials and conjunction



Suppose I have an existentially quantified formula of the form 
    EXISTS x: (p(x) AND q)
I want to simplify this to 
    (EXISTS x: p(x)) AND q

Easy enough, but in general I may have more than two terms and the
terms which mention the quantified variable will not necessarilly be
grouped.  E.g., I might have
    EXISTS x: (p1(x) AND q1 AND q2 AND p2(x))
which I want to simplify to 
    (EXISTS x: (p1(x) AND p2(x))) AND (q1 AND q2)

What is the best way to do this?

    Erika