alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tl: fix first_match definition

Browse source 
* doc/tl/tl.tex: Here.
This commit is contained in:
Alexandre Duret-Lutz 2021-12-14 14:18:53 +01:00
parent 4dc6bb08a2
commit e7f0df048a
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
doc/tl/tl.tex
View file

@ -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: