From 4629d074ab0b1374c9c055b8b1285a8e371fd843 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 7 Dec 2022 11:26:51 +0100
Subject: [PATCH] Fix semantics of [*i..j] and [:*i..j]

* doc/tl/tl.tex: After a discussion with Antoin, it appears that the
semantics previously given for f[*0..j] was not considering that f[*0]
should accept any sequence of one letter.
---
 doc/tl/tl.tex | 24 +++++++++---------------
 1 file changed, 9 insertions(+), 15 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 62a35635f..f9205cced 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -668,20 +668,17 @@ $a$ is an atomic proposition.
   \sigma\VDash f\FUSION g&\iff \exists k\in\N,\,(\sigma^{0..k} \VDash f)\land(\sigma^{k..} \VDash g)\\
   \sigma\VDash f\STAR{\mvar{i}..\mvar{j}}& \iff
   \begin{cases}
-    \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\
-    \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\,
-      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
-      \VDash f\STAR{\mvar{0}..\mvar{j-1}}))\\
+    \text{either} & \mvar{i}=0 \land\mvar{j}=0\land \sigma=\varepsilon \\
+    \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land \bigl((\sigma = \varepsilon) \lor (\sigma
+      \VDash f\STAR{\mvar{1}..\mvar{j}})\bigr)\\
     \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
       (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
       \VDash f\STAR{\mvar{i-1}..\mvar{j-1}}))\\
   \end{cases}\\
   \sigma\VDash f\STAR{\mvar{i}..} & \iff
   \begin{cases}
-    \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\
-    \text{or} & \mvar{i}=0 \land (\exists k\in\N,\,
-      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
-      \VDash f\STAR{\mvar{0}..}))\\
+    \text{either} & \mvar{i}=0 \land \bigl((\sigma=\varepsilon)\lor(\sigma
+      \VDash f\STAR{\mvar{1}..})\bigr)\\
     \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
       (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
       \VDash f\STAR{\mvar{i-1}..}))\\
@@ -689,19 +686,16 @@ $a$ is an atomic proposition.
   \sigma\VDash f\FSTAR{\mvar{i}..\mvar{j}}& \iff
   \begin{cases}
     \text{either} & \mvar{i}=0 \land \mvar{j}=0 \land \sigma\VDash\1 \\
-    \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\,
-      (\sigma^{0..k}\VDash f) \land (\sigma^{k..}
-      \VDash f\FSTAR{\mvar{0}..\mvar{j-1}}))\\
+    \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land \bigl((\sigma\VDash\1)\lor(\sigma
+      \VDash f\FSTAR{\mvar{1}..\mvar{j}})\bigr)\\
     \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
       (\sigma^{0..k}\VDash f) \land (\sigma^{k..}
       \VDash f\FSTAR{\mvar{i-1}..\mvar{j-1}}))\\
   \end{cases}\\
   \sigma\VDash f\FSTAR{\mvar{i}..} & \iff
   \begin{cases}
-    \text{either} & \mvar{i}=0 \land \sigma\VDash\1 \\
-    \text{or} & \mvar{i}=0 \land (\exists k\in\N,\,
-      (\sigma^{0..k}\VDash f) \land (\sigma^{k..}
-      \VDash f\FSTAR{\mvar{0}..}))\\
+    \text{either} & \mvar{i}=0 \land \bigl((\sigma\VDash\1)
+                    \lor(\sigma \VDash f\FSTAR{\mvar{1}..})\bigr)\\
     \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
       (\sigma^{0..k}\VDash f) \land (\sigma^{k..}
       \VDash f\FSTAR{\mvar{i-1}..}))\\