Re: [Core][PRD] Definition of safeness

Hi Stella,

Thanx. I made the corrections. Additional comments in-lined below.

Stella Mitchell <stellamit@gmail.com> wrote on 18/06/2009 18:50:30:
>  
> The definition of safeness of a variable in a condition formula 
> doesn't cover the case where the condition formula is an existential 
formula.

You are right: the case was not in Jos's definition, because existential 
quantifiers were completely removed. But they were added back in the 
bottom-up definition, to ease the extension to PRD...

I added the clause that "v is safe in an existential formula, Exists 
v1...vn (f), iff it is safe in f."
 
>     Last para:
>         what is the significance of  "...that is, even if F is a 
> disjunction" at the end?

Nothing. I thought that I had removed it already :-( Now, it *is* removed, 
anyway.

Cheers,

Christian

Sauf indication contraire ci-dessus:/ Unless stated otherwise above:
Compagnie IBM France
Siège Social : Tour Descartes, 2, avenue Gambetta, La Défense 5, 92400 
Courbevoie
RCS Nanterre 552 118 465
Forme Sociale : S.A.S.
Capital Social : 609.751.783,30 ?
SIREN/SIRET : 552 118 465 02430