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?