In reply to scfabchiang:
ap_never_succeed: assert property(
($rose(a) ##[2:$] b) |=> c);
// The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(
($rose(a) ##2 b)or // NOTE: The ORing is in the antecedent
($rose(a) ##3 b)or
…
($rose(a) ##n b)|=> c); // where n is infinity
// Thus for failure, all you need is any of the antecedent thread to match and
// its corresponding consequent to be a nonmatch
// If any antecedent of thoses threads is a nonmatch, then that thread is vacuously TRUE.
// You wrote "//my understanding
/* ap_equivalent_to_ap_never_succeed_mod: assert property(
($rose(a) ##2 b) and
($rose(a) ##3 b) and
…
($rose(a) ##n b)|=> c); // where n is infinity */
// [Ben] NO, you are incorrect. With your ANDind assumption of
// ANDing all threads of the antecedent, if any thread of the antecedent is a nonmatch
// then the assertion is vacously trrue.
// (1 and 1 and 0 and 1 ... and (whatever) |=> 1 // is vacuously true
//For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed,
// and there are an infinite number of threads; specifically, these threads include:
// ANOTHER way of seeing the treads
(($rose(a) ##2 b) |=> c) and // thread 1 property
(($rose(a) ##3 b) |=> c) and // thread 2 property
…
(($rose(a) ##n b)|=> c) // thread n
// "all thread must succeed to succeed the assertion"
// The ANDing is in the equivalent property threds
// I had the ORing in the antecedent threads.
// Different way of looking at it.