Click here for the answer.
Sometimes I get so used to dealing with synchronous assertions that I forget there’s a large portion of the community that uses asynchronous assertions. In many ways, asynchronous assertions are easier to deal with formally than synchronous ones. Check out the logic above, and see what you think you might do.
f_past_valid is defined like I normally define it: