[sv-ac] Re: JH comments on 1932 Annex F changes

Hi Doron:

> >>* p. 6, F.2.3.2.8.  I think that
> >>
> >>     s_eventually[m:$] p \equiv not(always[m:$] not p)
> >>
> >>  should be a theorem.  Would this make a better definition?
> 
> [[DB:]] I constructed the definitions this way so that all strong
> operators are derived using "not". This makes the recursive properties
> definitions easier, because it does not need to consider strong
> operators.

I don't think my point was clear.  I meant that I think

   s_eventually[m:$] p \equiv not(always[m:$] not p)

_IS_ a theorem based on your definition, however I have not checked
it carefully.  

Your definition currently says

   s_eventually[m:$] p \equiv (s_next[m] s_eventually p)


I am suggesting that you consider changing this definition to 

   s_eventually[m:$] p \equiv not(always[m:$] not p)

because of the similarity of this form to your other definitions.

J.H.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.