An LTL formula is true of a stream of states. A stream of states might usually
be modelled as a function from numbers to states. However, in the development
you're referring to, the states are just numbers, so that the first state of the
stream is number 0, the next is number 1 etc. Moreover, th
Hello,
I am very new, started yesterday, to HOL (in fact to theorem
proving itself). I was looking forward to use the Temporal logic
theory in HOL4, but I have a problem:
The definition of NEXT |- !P. NEXT P = \t. P (SUC t) seems a bit
odd.
