famubu
/
playground
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[tex] add turnstile usage example

This commit is contained in:
Julin S 2024-02-28 13:16:55 +05:30
parent 8d30806189
commit 9fa9777064
1 changed files with 60 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

60
latex/turnstile-package.tex Normal file
View File

@ -0,0 +1,60 @@
\documentclass{article}
\usepackage{mathpartir}
\usepackage{turnstile}
% \newcommand{\vDdash}{\sttstile{}{}} % three horizontal stripe models symbol
\newcommand{\modelsere}{\sttstile{}{}} % three horizontal stripe models symbol
\newcommand{\modelbool}{\ddtstile{}{}} % two horizontal stripe models symbol
\newcommand{\modelppty}{\sdtstile{}{}} % three horizontal stripe models symbol
\begin{document}
\begin{figure}
\begin{mathpar}
\begin{array}{rclcl}
w & \modelsere & \varepsilon & \iff & w = nil \\
w & \modelsere & b & \iff & |v| = 1 \ \land \ v[0] \modelbool b \\
w & \modelsere & r1;r2 & \iff & \exists w1 \ w2, \
w=w1 \cdot w2 \ \land \
w1 \modelsere r1 \ \land \
w2 \modelsere r2 \\
w & \modelsere & r1|r2 & \iff & w \modelsere r1 \ \lor \
w \modelsere r2 \\
w & \modelsere & r1:r2 & \iff & \exists w1 \ a \ w2, \
w=w1 \cdot [a] \cdot w2 \land
w1 \cdot [a] \modelsere r1 \land
[a] \cdot w2 \modelsere r2 \\
w & \modelsere & r1 \&\& r2 & \iff & w \modelsere r1 \land w \modelsere r2 \\
w & \modelsere & r* & \iff & w \modelsere \varepsilon \ \lor
\exists w1 w2, w = w1 \cdot w2 \land
w1 \neq nil \land
w1 \modelsere r \land
w2 \modelsere r* \\
\end{array}
\end{mathpar}
\caption{SERE semantics}
\end{figure}
\begin{figure}
\begin{mathpar}
\begin{array}{lcl}
w \modelppty r & \iff & w \modelsere r \\
w \modelppty \lnot p & \iff & w \not \modelppty p \\
w \modelppty p \land q & \iff & w \modelppty p \ \land w \modelppty q \\
w \modelppty r \mapsto p & \iff & \forall j < |w|,
w[0:j] \modelsere r \land
w[j \kern-0.2em :] \modelppty p \\
w \modelppty X \ p & \iff & |w| > 1 \land
w[1 \kern-0.2em :] \modelppty p \\
w \modelppty p \ U q & \iff & \exists j < |w|,
w[j \kern-0.2em :] \modelppty q \land
\forall k < j,
w[k \kern-0.2em :] \modelppty p \\
\end{array}
\end{mathpar}
\caption{Property semantics}
\end{figure}
\end{document}