From b860bb242e28c10f4a2c8b51ab30692b13b98b95 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Dec 2021 14:18:53 +0100 Subject: [PATCH] tl: fix first_match definition * doc/tl/tl.tex: Here. --- doc/tl/tl.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 39e0f1f48..2c0599f82 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -707,7 +707,7 @@ $a$ is an atomic proposition. \VDash f\FSTAR{\mvar{i-1}..}))\\ \end{cases}\\ \sigma\VDash \FIRSTMATCH\code(f\code) & \iff - (\sigma\VDash f)\land (\nexists k<|\sigma|,\,\sigma^{0..k}\nVDash f) + (\sigma\VDash f)\land (\forall k<|\sigma|,\,\sigma^{0..k}\nVDash f) \end{align*}} Notes: