Fixes

diff --git a/ac_notes.tex b/ac_notes.tex
index aa11df8bb7b75214c8cceed33e8efa083d15d6be..498812eab9a78b14566e9f0de8fc43d4fb361995 100644 (file)
--- a/ac_notes.tex
+++ b/ac_notes.tex
@@ -13,27 +13,29 @@
 \r
 \maketitle\r
 \r
+\newcommand{\Prgm}[2]{[#1\Comma #2]}\r
+\r
 \subparagraph{Syntax}\r
 \[\begin{array}{lll}\r
-  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\\r
-  n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\\r
+  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \Prgm{\tm}{\vec\tm} \\\r
+  n & \ddef & \Lam\var \Prgm{n}{\vec n} \mid \var\,\vec n \\\r
   \\\r
   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
-  P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm  \\\r
-  \tilde P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
+  P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
 \end{array}\]\r
 \r
 \subparagraph{Reduction}\r
 \[\begin{array}{lll}\r
-  P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} &\r
-   P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\\r
-   P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} &\r
-    P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\\r
+  P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\in \Prgm\tm{\vec\tm}} &\r
+   P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
+   P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\Prgm\tm{\vec\tm}} &\r
+    P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
 \end{array}\]\r
 \r
 \subparagraph{Properties of the calculus:}\r
 \begin{itemize}\r
   \item Every term is normalizing iff it is strongly normalizing.\r
+  \item Ogni strategia e' perpetua!\r
 \end{itemize}\r
 \r
 \clearpage\r