--- 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)))