for secu
authorChengsong
Wed, 05 Feb 2020 10:58:13 +0000
changeset 115 5c8afe4a8090
parent 114 dd7f719c451d
child 116 dfcad6f19e06
for secu
etnms/etnms.tex
--- a/etnms/etnms.tex	Wed Feb 05 10:45:15 2020 +0000
+++ b/etnms/etnms.tex	Wed Feb 05 10:58:13 2020 +0000
@@ -397,18 +397,18 @@
 \begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
   $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
   $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
-  $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
+  $\textit{decode}'\,(0\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
      $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
        (\Left\,v, bs_1)$\\
-  $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
+  $\textit{decode}'\,(1\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
      $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
        (\Right\,v, bs_1)$\\                           
   $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
         $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
   & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
   & &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
-  $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
-  $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & 
+  $\textit{decode}'\,(0\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
+  $\textit{decode}'\,(1\!::\!bs)\,(r^*)$ & $\dn$ & 
          $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
   & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
   & &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
@@ -428,12 +428,12 @@
 
 \begin{center}
 \begin{tabular}{lcl}
-  $\textit{a}$ & $::=$  & $\textit{ZERO}$\\
-                  & $\mid$ & $\textit{ONE}\;\;bs$\\
-                  & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
-                  & $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
-                  & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
-                  & $\mid$ & $\textit{STAR}\;\;bs\,a$
+  $\textit{a}$ & $::=$  & $\ZERO$\\
+                  & $\mid$ & $_{bs}\ONE$\\
+                  & $\mid$ & $_{bs}{\bf c}$\\
+                  & $\mid$ & $_{bs}\oplus\,as$\\
+                  & $\mid$ & $_{bs}a_1\cdot a_2$\\
+                  & $\mid$ & $_{bs}a^*$
 \end{tabular}    
 \end{center}  
 %(in \textit{ALTS})