diff --git a/latex/turnstile-package.tex b/latex/turnstile-package.tex
new file mode 100644
index 0000000..47daac4
--- /dev/null
+++ b/latex/turnstile-package.tex
@@ -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}