Hi John, I understand now. I think that the theorem is true. I also think that the current definition is clearer. There is some balance here between clarity, conscience (I could write clearer definitions using auxiliary definitions like s_eventualy[m:m],) and wanting to derive all strong operators using not. I am happy with the way things are right now. Doron >>-----Original Message----- >>From: John Havlicek [mailto:john.havlicek@freescale.com] >>Sent: Monday, January 14, 2008 2:29 PM >>To: Bustan, Doron >>Cc: john.havlicek@freescale.com; sv-ac@eda.org >>Subject: 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.Received on Mon Jan 14 05:21:02 2008
This archive was generated by hypermail 2.1.8 : Mon Jan 14 2008 - 05:21:29 PST