diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 289c4fdc6..b358ec940 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -785,11 +785,12 @@ omitted.
   f\DELAYR{0..}g                & \equiv (f\FUSION{}g)\OR(f\CONCAT{}\1\STAR{}\CONCAT{}g)\quad\text{if~}\varepsilon\VDash f \land \varepsilon\VDash g
 \end{align*}
 \begin{align*}
-  f\DELAY{\mvar{i}} g           & \equiv f\DELAYR{\mvar{i}..\mvar{i}} g & {}\DELAY{\mvar{i}} g  & \equiv \1\DELAYR{\mvar{i}..\mvar{i}} g                          \\
-  f\DELAYP{}g                   & \equiv f\DELAYR{1..}g                 & \DELAYP{} g           & \equiv\DELAYR{1..}g                                             \\
-  f\DELAYS{}g                   & \equiv f\DELAYR{0..}g                 & \DELAYS{} g           & \equiv\DELAYR{0..}g
-  f\DELAYR{..\mvar{j}} g        & \equiv f\DELAYR{0..\mvar{j}} g\}      & \DELAYR{..\mvar{j}} g & \equiv \1\DELAYR{0..\mvar{j}} g\}                               \\
-  f\DELAYR{..} g                & \equiv f\DELAYR{0..} f g\}            & \DELAYR{..} g         & \equiv \1\DELAYR{0..} g\}                                       \\
+  \DELAYR{\mvar{i}..\mvar{j}}g  & \equiv \1\STAR{\mvar{i}..\mvar{j}}\CONCAT g & \DELAYR{\mvar{i}..}g  & \equiv \1\STAR{\mvar{i}..}\CONCAT g                       \\
+  f\DELAY{\mvar{i}} g           & \equiv f\DELAYR{\mvar{i}..\mvar{i}} g       & {}\DELAY{\mvar{i}} g  & \equiv \1\STAR{\mvar{i}}\CONCAT g                         \\
+  f\DELAYP{}g                   & \equiv f\DELAYR{1..}g                       & \DELAYP{} g           & \equiv\DELAYR{1..}g                                       \\
+  f\DELAYS{}g                   & \equiv f\DELAYR{0..}g                       & \DELAYS{} g           & \equiv\DELAYR{0..}g                                       \\
+  f\DELAYR{..\mvar{j}} g        & \equiv f\DELAYR{0..\mvar{j}} g\}            & \DELAYR{..\mvar{j}} g & \equiv \1\DELAYR{0..\mvar{j}} g\}                         \\
+  f\DELAYR{..} g                & \equiv f\DELAYR{0..} f g\}                  & \DELAYR{..} g         & \equiv \1\DELAYR{0..} g\}
 \end{align*}
 
 \subsection{Trivial Identities (Occur Automatically)}
diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy
index 0d7e7dd87..64c97ae1e 100644
--- a/spot/parsetl/parsetl.yy
+++ b/spot/parsetl/parsetl.yy
@@ -541,8 +541,7 @@ sere: booleanatom
 	    | sere OP_FUSION error
               { missing_right_binop($$, $1, @2, "fusion operator"); }
 	    | OP_DELAY_N sere
-              { $$ = formula::sugar_delay(formula::tt(), formula($2),
-                                          $1, $1).to_node_(); }
+              { $$ = formula::sugar_delay(formula($2), $1, $1).to_node_(); }
 	    | OP_DELAY_N error
               { missing_right_binop($$, fnode::tt(), @1, "SVA delay operator"); }
 	    | sere OP_DELAY_N sere
@@ -557,7 +556,7 @@ sere: booleanatom
 		    error_list.emplace_back(@1, "reversed range");
 		    std::swap($1.max, $1.min);
 		  }
-                $$ = formula::sugar_delay(formula::tt(), formula($2),
+                $$ = formula::sugar_delay(formula($2),
                                           $1.min, $1.max).to_node_();
               }
 	    | delayargs error
diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc
index f31c974b5..b72a61a34 100644
--- a/spot/tl/formula.cc
+++ b/spot/tl/formula.cc
@@ -1773,15 +1773,22 @@ namespace spot
     return Concat({Star(Concat({s, b}), min, max), s});
   }
 
+  formula formula::sugar_delay(const formula& b,
+                               unsigned min, unsigned max)
+  {
+    // ##[min:max] b = 1[*min:max];b
+    return Concat({Star(tt(), min, max), b});
+  }
   formula formula::sugar_delay(const formula& a, const formula& b,
                                unsigned min, unsigned max)
   {
     // If min>=1
     //   a ##[min:max] b  = a;1[*min-1:max-1];b
     // If min==0 we can use
-    //   a ##[min:max] b = a:(1[*0:max];b)  if a rejects [*0]
-    //   a ##[min:max] b = (a;1[*0:max]):b  if b rejects [*0]
-    //   a ##[min:max] b = (a:b)|(a;[*0:max-1];b)  else
+    //   a ##[0:0] b = a:b
+    //   a ##[0:max] b = a:(1[*0:max];b)  if a rejects [*0]
+    //   a ##[0:max] b = (a;1[*0:max]):b  if b rejects [*0]
+    //   a ##[0:max] b = (a:b)|(a;[*0:max-1];b)  else
     if (min > 0)
       {
         --min;
@@ -1789,6 +1796,8 @@ namespace spot
           --max;
         return Concat({a, Star(tt(), min, max), b});
       }
+    if (max == 0)
+      return Fusion({a, b});
     if (!a.accepts_eword())
       return Fusion({a, Concat({Star(tt(), 0, max), b})});
     if (!b.accepts_eword())
diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh
index cf16accb3..f45681103 100644
--- a/spot/tl/formula.hh
+++ b/spot/tl/formula.hh
@@ -1245,9 +1245,25 @@ namespace spot
     ///
     /// The operator does not exist in Spot it is handled as syntactic
     /// sugar by the parser.  This function is used by the parser to
-    /// create the equivalent SERE.
+    /// create the equivalent SERE using PSL operators.
+    ///
+    /// The rewriting rules depends on the values of a, n, and b.
+    /// If n≥1 `a ##[n:m] b` is encoded as `a;1[*n-1,m-1];b`.
+    /// Otherwise:
+    /// * `a ##[0:0] b` is encoded as `a:b`,
+    /// * For m>0, `a ##[0:m] b` is encoded as
+    ///   - `a:(1[*0:m];b)` is `a` rejects `[*0]`,
+    ///   - `(a;1[*0:m]):b` is `b` rejects `[*0]`,
+    ///   - `(a:b) | (a;1[*0:m-1];b)` is `a` and `b` accept `[*0]`.
+    ///
+    /// The left operand can also be missing, in which case
+    /// `##[n:m] b` is rewritten as `1[*n:m];b`.
+    /// @{
     static formula sugar_delay(const formula& a, const formula& b,
                                unsigned min, unsigned max);
+    static formula sugar_delay(const formula& b,
+                               unsigned min, unsigned max);
+    /// @}
 
 #ifndef SWIG
     /// \brief Return the underlying pointer to the formula.
diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test
index 5c10a1b0e..adfbdbc2d 100755
--- a/tests/core/ltlfilt.test
+++ b/tests/core/ltlfilt.test
@@ -58,6 +58,7 @@ F(a & !Xa & Xb)
 {a*;(!a)*;a[+]}|->b
 {a*;(!a)[+];a[+]}|->b
 {a*;(!c)[+];a[+]}|->b
+{a* ##0 b*}|->c
 EOF
 
 checkopt --boolean <<EOF
@@ -115,10 +116,11 @@ a & (b | c)
 {a[+];{!a}[*];a[*]}[]-> b
 {a[*];{!a}[*];a[+]}[]-> b
 {a[*];{!a}[+];a[+]}[]-> b
+{a[*]:b[*]}[]-> c
 EOF
 
 checkopt -c --stutter-invariant <<EOF
-15
+16
 EOF
 
 checkopt --syntactic-stutter-invariant <<EOF
@@ -134,6 +136,7 @@ a & (b | c)
 {a[*];{!a}[+];a[*]}[]-> b
 {a[+];{!a}[*];a[*]}[]-> b
 {a[*];{!a}[*];a[+]}[]-> b
+{a[*]:b[*]}[]-> c
 EOF
 
 checkopt --simplify <<EOF
@@ -158,6 +161,7 @@ a R (b W !a)
 !a R (a R (b W !a))
 !a R (a | X(a R (b W !a)))
 !a R (c | X(c R (b W !a)))
+(c W !b) W !a
 EOF
 
 checkopt --simplify --eventual --unique <<EOF
@@ -191,6 +195,7 @@ a & (b | c)
 {a[*];{!a}[*];a[+]}[]-> b
 {a[*];{!a}[+];a[+]}[]-> b
 {a[*];{!c}[+];a[+]}[]-> b
+{a[*]:b[*]}[]-> c
 EOF
 
 checkopt --obligation <<EOF
@@ -210,6 +215,7 @@ a & (b | c)
 {a[*];{!a}[*];a[+]}[]-> b
 {a[*];{!a}[+];a[+]}[]-> b
 {a[*];{!c}[+];a[+]}[]-> b
+{a[*]:b[*]}[]-> c
 EOF
 
 checkopt --guarantee <<EOF
@@ -232,6 +238,7 @@ checkopt -v --ltl <<EOF
 {a[*];{!a}[*];a[+]}[]-> b
 {a[*];{!a}[+];a[+]}[]-> b
 {a[*];{!c}[+];a[+]}[]-> b
+{a[*]:b[*]}[]-> c
 EOF
 
 checkopt -v --ap=3 <<EOF
@@ -275,6 +282,7 @@ a & (b | c)
 {a[*];{!a}[*];a[+]}[]-> b
 {a[*];{!a}[+];a[+]}[]-> b
 {a[*];{!c}[+];a[+]}[]-> b
+{a[*]:b[*]}[]-> c
 EOF
 
 checkopt -v --stutter-invariant <<EOF
diff --git a/tests/core/sugar.test b/tests/core/sugar.test
index 83fef3ef7..12cdfe0a2 100755
--- a/tests/core/sugar.test
+++ b/tests/core/sugar.test
@@ -37,12 +37,18 @@ F [2:4] a |  b
 F [4:2]a | F[2:2]b
 F[]a|G[]b|X[]c
 {a ##0 b ##1 c ##2 d}|->e
+{a* ##0 b* ##1 c* ##2 d*}|->e
 {(##2 a)[*] ##1 b}|->e
 {a ##[0:3] b}|->e
+{a* ##[0:3] b}|->e
+{a ##[0:3] b*}|->e
+{a* ##[0:3] b*}|->e
 {a ##[1..] b}|->e
 {a ##[:] b}|->e
 {a ##[:1] b}|->e
 {##[..3] b}|->e
+{##[0..2] b*}|->e
+{##[1..2] b*}|->e
 {a ##[+] b}|->e
 {##[*] b}|->e
 EOF
@@ -62,12 +68,18 @@ b | XX(a | X(a | Xa))
 XX(a | X(a | Xa)) | XXb
 FGa | Gb | XGc
 {{a && b};c;1;d}[]-> e
+{{a[*]:b[*]};c[*];1;d[*]}[]-> e
 {{[*2];a}[*];b}[]-> e
 {a:{[*0..3];b}}[]-> e
+{{a[*];[*0..3]}:b}[]-> e
+{a:{[*0..3];b[*]}}[]-> e
+{{a[*]:b[*]} | {a[*];[*0..2];b[*]}}[]-> e
 {a;[*];b}[]-> e
 {a:{[*];b}}[]-> e
 {a:{[*0..1];b}}[]-> e
 {[*0..3];b}[]-> e
+{[*0..2];b[*]}[]-> e
+{[*1..2];b[*]}[]-> e
 {a;[*];b}[]-> e
 {[*];b}[]-> e
 EOF