[$ieee-1850] {a[*0] : b } // No match?

I found this in:
http://www.verificationguild.com/modules.php?name=Forums&file=viewtopic&p=2339#2339

An empty sequence is one that does not match over any positive number
of clocks. The following rules apply
for concatenating sequences with empty sequences. An empty sequence is
denoted as empty and a sequence is
denoted as seq.
— (empty ##0 seq) does not result in a match
— (seq ##0 empty) does not result in a match
— (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq)
— (seq ##n empty), where n is greater than 0, is equivalent to (seq
##(n-1) 'true)
We have a similar situation in PSL with the fusion operator instead of the ##0.
I don't believe the PSL LRM defines what happens in such circumstances.
Consider the sequence {a[*0] : b }
Fusion is defined as 2 sequences overlapping by one cycle.
If one of those cycles is empty (i.e., need not exist, then what?
SVA defines that as a NO MATCH.
Ben

-- 
--------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 
http://www.vhdlcohen.com/  ben@abv-sva.org
* Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
* Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd
Edition, 2004, ISBN 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
---------------------------------------------------------------------------