[sv-ac] [SV-AC] F.5.3.3 Vacuity // Clarification on "implies" and suggestion

F.5.3.3 Vacuity states: An evaluation of P on w is nonvacuous provided w P.
w non-vacuous on "P1 implies P2" iff w is non-vacuous on P1.
I can't type the symbology, but I don't quite understand it totally.
But, if I understand it correctly,
 "P1 implies P2" is vacuous if P1 is vacuous; correct?
If P1 is a sequence, it is never vacuous. Yet wouldn't it be desirable to
have the property "P1 implies P2" be vacuous if the antecedent if false,
like the implication operator?
Thus, I could write something like:
sequence t; 1; endsequence
sequence t1; t ##1 1; endsequence
sequence t4; t ##4 1; endsequence
property P;
   (t ##0 a) implies
     (t ##0 b) and
     (t1 ##0 c) and
     (t4 ##0 d);
endproperty

Please, don't educate me on how to write this with the implication operator;
that is not my point.
My point is that this is another style where I want to use the "implies"
operator, yet, if the antecedent if false, I don't want the property P to
be TRUE non-vacuously. In simulation, the success count would be high.
Question: Do we want to entertain the idea of an "implies" property to be
vacuous if the antecedent is false?
The "p1implies p2" is same as "(not p1) or p2".
Ben Cohen

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.