Unexpected behaviour of implication operator in SVA

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks a lot for the reply.
It would be very grateful if you can also explain my doubt below.

At time 45, the sampled value of ‘state’ is ‘STATE3’, so I am really confused as to how the sequence s2_7 did even start.

Thanks
Abhay