Another quite similar relation is ‘Await’ where O = A await n is an output that ticks only once when the nth tick of A arrives, and then dies forever. Here is my interpretation for this (with n = 5):
$rose(rst) |=> ( (a[=5]) intersect (!o[*]) ) ##1 ( $rose(a) && $rose(o) ) ##1 ( (a[=1:$]) intersect !o[*] ) ;
Here as per your book, a[=2] is equivalent to
!a[*0:$] ##1 a ##1 !a[*0:$] ##1 a ##1 !a[*0:$]
then it seems quite OK but in practice it doesn’t work. May be you can help!