# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1384892359 0
# Node ID 058504a45c34fc4d94db1398399157d575aa1319
# Parent  e78af5feb655a5056fdf8433be7be231b417e9ea
added

diff -r e78af5feb655 -r 058504a45c34 progs/prove.scala
--- a/progs/prove.scala	Tue Nov 19 03:05:48 2013 +0000
+++ b/progs/prove.scala	Tue Nov 19 20:19:19 2013 +0000
@@ -62,6 +62,9 @@
     case True => sc ()
     case False => ()
     case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
+    case Says(p, Enc(f1, f2)) => 
+      prove(j.lhs |- Says(p, f1), 
+            () => prove(j.lhs |- Says(p, f2), sc))
     case Says(p, f1) => prove(j.lhs |- f1, sc) 
     case Or(f1, f2) => 
       { prove(j.lhs |- f1, sc);
@@ -70,7 +73,6 @@
       prove(j.lhs |- f1, 
             () => prove(j.lhs |- f2, sc))
     case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc)
-    case Enc(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
     case _ => ()
   }
 
@@ -92,6 +94,9 @@
     case Or(f1, f2) => 
       prove(lhs_rest + f1 |- rhs, 
             () => prove(lhs_rest + f2 |- rhs, sc))
+    case Says(p, Enc(f1, f2)) => 
+      prove(lhs_rest |- Says(p, f2), 
+            () => prove(lhs_rest + Says(p, f1) |- rhs, sc))
     case Says(p, Imp(f1, f2)) => 
       prove(lhs_rest |- Says(p, f1), 
             () => prove(lhs_rest + Says(p, f2) |- rhs, sc))
@@ -141,10 +146,6 @@
 
 println("Server Example")
 
-val Alice = "Alice"
-//val Bob = "Bob"  -- already defined
-val Server = "Server"
-
 def Connect(p: String, q: String) : Form =
   Pred("Connect", List(Var(p), Var(q)))
 
diff -r e78af5feb655 -r 058504a45c34 slides/slides07.pdf
Binary file slides/slides07.pdf has changed
diff -r e78af5feb655 -r 058504a45c34 slides/slides07.tex
--- a/slides/slides07.tex	Tue Nov 19 03:05:48 2013 +0000
+++ b/slides/slides07.tex	Tue Nov 19 20:19:19 2013 +0000
@@ -450,8 +450,8 @@
   \frametitle{Sending Rule}
 
   \bl{\begin{center}
-  \mbox{\infer{\Gamma \vdash Q \;\text{says}\; F}
-              {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}}
+  \mbox{$\infer{\Gamma \vdash Q \;\text{says}\; F}
+              {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}$}
   \end{center}}\bigskip\pause
   
   \bl{$P \,\text{sends}\, Q : F \dn$}\\