--- a/programs/prove1.scala	Tue Oct 30 14:48:13 2012 +0000
+++ b/programs/prove1.scala	Tue Oct 30 21:13:36 2012 +0000
@@ -24,7 +24,6 @@
 val Bob = "Bob"
 val Del = Pred("del_file", Nil)
 
-
 val Gamma = 
   List( Says(Admin, Del) -> Del,
         Says(Admin, Says(Bob, Del) -> Del),
@@ -37,11 +36,13 @@
   else prove1(j.lhs, j.rhs, sc) 
 }
 
-def partitions(ls: List[Form]): List[(Form, List[Form])]  = 
+def partitions[A](ls: List[A]): List[(A, List[A])]  = 
   ls.map (s => (s, ls - s))
 
 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
   rhs match {
+    case True => sc()
+    case False => ()
     case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 
     case Says(p, f1) => prove(Judgement(lhs, f1), sc) 
     case Or(f1, f2) => 
@@ -56,6 +57,8 @@
 
 def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 
   f match {
+    case True => prove(Judgement(lhs_rest, rhs), sc)
+    case False => sc()
     case And(f1, f2) =>
       prove(Judgement(f1::f2::lhs_rest, rhs), sc)
     case Imp(f1, f2) => 
@@ -81,11 +84,25 @@
   catch { case e: Exception => () }
 } 
 
+run (Judgement (Nil, False -> Del))
+run (Judgement (Nil, True -> Del))
+run (Judgement (Nil, Del -> True))
+
 run (goal)
 
+val Gamma1 = 
+  List( Says(Admin, Says(Bob, Del) -> Del),
+        Says(Bob, Del) )
+
+val goal1 = Judgement(Gamma1, Del) // not provable
+
+run (goal1)
 
 run (Judgement(Nil, Del -> Del))
 
+run (Judgement(Nil, Del -> Or(False, Del)))
+
+
 val Chr = "Christian"
 val HoD = "Michael Luck"
 val Email = Pred("may_btain_email", List(Const(Chr)))