Click here for the answer.
As with all my examples, I define
I use this to make certain I never make assertions about
$past(X) on the first
clock, given that such assertions would reference a value of
X before the
initial time step–a time when it’s undefined.
As for the rest of the question, bear in mind that I’m known to ask trick questions and this question is no different.