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

Re: Hourly clock spec: why it needs the temporal-logic operator box []

You say that HCnxt is, by definition, always true.  By that reasoning, if the spec had defined HCini to equal hr = 1, would that always be true?  How would you specify an hour clock that had to begin with hr = 1?  And if I were to write the definition

   FalseTheorem == 1+2 = 4

would that mean that 1+2 = 4 is always true?  What is the difference between a definition and a theorem?