[tex] add another example in misc.tex

.gitignore

@@ -70,3 +70,4 @@ lex.yy.c
 bsv/**/bsim
 bsv/**/*.h
 
+latex/**.pdf

latex/misc.tex

@@ -19,4 +19,25 @@
   \caption{Antimirov derivatives}
   \label{fig:antimirov}
   \end{figure}
+
+  \begin{figure}[h]
+  \begin{mathpar}
+  \begin{array}{rcl}
+    w \models \varepsilon & \iff & w = nil                       \\
+    w \models b           & \iff & (|w|=1) \land (w_0 \models b) \\
+    w \models (r_1 ; r_2) & \iff & (w=w_1 \cdot w_2) \land
+                                   (w_1 \models r_1) \land
+                                   (w_2 \models r_2)             \\
+    w \models (r_1 + r_2) & \iff & (w \models r_1) \ \lor \
+                                   (w \models r_2)               \\
+    w \models r*          & \iff & (w \models \varepsilon) \ \lor \ 
+                                   (w=w_1 \cdot w_2) \land
+                                   (w_1 \models r) \land
+                                   (w_2 \models r*)              \\
+  \end{array}
+  \end{mathpar}
+  \caption{Semantics of regular expression}
+  \label{fig:re-semantics}
+  \end{figure}
+
 \end{document}

latex/nfa-rules.tex

@@ -0,0 +1,82 @@
+\documentclass{article}
+\usepackage{mathpartir}
+
+\begin{document}
+
+\begin{figure}
+  \begin{mathpar}
+    \inferrule{ }{
+fin \notin \delta_\emptyset^*(s, w) 
+    }
+    \quad (\textsc{Null})
+%
+    \quad \quad
+    \inferrule{ }{
+fin \in \delta_\epsilon^*(fin, \epsilon) 
+    }
+    \quad (\textsc{Eps})
+%
+\and
+    \inferrule{
+fin \in \delta_a(s, [a])
+    }{
+fin \in \delta_a^*(s, [a])
+    }
+    \quad (\textsc{Char})
+%
+\and
+%
+    \inferrule{
+fin_1 \in \delta_1^*(s, w_1)
+  \and
+fin_2 \in \delta_1^*(fin_1, w_2)
+    }{
+fin_{1 \cdot 2} \in \delta_{1 \cdot 2}^*(s, w_1 \cdot w_2)
+    }
+    \quad (\textsc{Cat})
+%
+\and
+\\
+    \inferrule{
+fin_1 \in \delta_1^*(s, w)
+    }{
+fin \in \delta_{1 + 2}^*(s, w)
+    }
+    \quad (\textsc{Alt-L})
+%
+\and
+%
+    \inferrule{
+fin_2 \in \delta_2^*(s, w)
+    }{
+fin \in \delta_{1 + 2}^*(s, w)
+    }
+    \quad (\textsc{Alt-R})
+%
+\and
+\\
+    \inferrule{
+fin_r \in \delta_r^*(s, w)
+    }{
+fin \in \delta_{r+}^*(s, w)
+    }
+    \quad (\textsc{Plus-1})
+%
+\and
+%
+    \inferrule{
+fin_r \in \delta_r^*(s, w_1)
+  \and
+fin_{r+} \in \delta_{r+}^*(fin_r, w_2)
+    }{
+fin \in \delta_{r+}^*(s, w_1 \cdot w_2)
+%fin \in \delta_{r+}^*(s, w_1 ++ w_2)
+%fin \in \delta_{r+}^*(s, w_1 \mathbin{{+}{+}} w_2)
+    }
+    \quad (\textsc{Plus-*})
+    \end{mathpar}
+  \caption{Typing rules}
+  \label{fig:nfa_typing}
+\end{figure}
+
+\end{document}