Nested Implication

In both cases, after a successful attempt (i.e., start==1) if send is false 2 ticks later, the assertion is vacuous. In the 2nd case (start ##2 send |-> ##3 ack );the assertion is vacuous because the antecedent is a no match. In the 1st case, it is vacuous (true vacuously) because the property that follows the start is vacuous.
Ben Cohen systemverilog.us