Question on Sequence concatenation '##'

Hello Forum,
I am writing a SVA for following

There are 2 variables ‘a’ & ‘b’. After 3 clock cycles ‘b’ should have same value as ‘a’

My 1st attempt works fine

 property p1; 
    int  local_data;
   @(posedge clk) ( 1 , local_data = a ) ##3  ( b == local_data ) ; 
  endproperty

  ap1_test: assert property( p1 )  $display("Pass at time: %2t", $time );
                             else  $error("Failure at time:%2t" , $time ); 

As an alternative I tried ::

 property p2; 
    int  local_data;
   @(posedge clk) ( 1 , local_data = a ) |-> ##3 ( b == local_data );  //  Why is consequent Legal ?
  endproperty

 ap2_test: assert property( p2 )  $display("Pass at time: %2t", $time );
                            else  $error("Failure at time:%2t" , $time );

I am confused on the working of the consequent. As per LRM

Sequences can be composed by concatenation, analogous to a concatenation of lists.
The concatenation specifies a delay, using ##, from the end of the first sequence until the beginning of the second sequence

Since ‘##N’ is used between 2 sequence expressions, and the consequent has only 1 sequence expression i.e ( b == local_data ),
I believed that it should result in compilation error (although the code is legal when I simulated)

To make it legal one should add an always true sequence expression (1)

 property p2; 
    int  local_data;
   @(posedge clk) ( 1 , local_data = a ) |-> 1 ##3 ( b == local_data );  //  1 is seqeunce expression
  endproperty

 ap2_test: assert property( p2 )  $display("Pass at time: %2t", $time );
                            else  $error("Failure at time:%2t" , $time );

Why is the consequent ’ ##3 ( b == local_data ); ’ considered legal even though there is no sequence expression preceding ##3 ?

Look at the BNF ofa sequence and a property:


sequence_expr ::=
   cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
 | ---

property_expr ::=
   sequence_expr 
   ...
  | sequence_expr |-> property_expr
  | ...
 thus  seq |-> ##3 seq2  is legal because it complies to the notation