--- a/scala/recs.scala	Mon Apr 22 10:33:40 2013 +0100
+++ b/scala/recs.scala	Wed Apr 24 09:49:00 2013 +0100
@@ -41,9 +41,19 @@
 case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
   override def eval(ns: List[Int]) = 
     if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
-    else throw new IllegalArgumentException("Cn args: " + ns + "," + n)
+    else { 
+      val msg = List("Cn f: " + f, 
+                     "n: " + n,
+                     "f arity: " + f.arity, 
+                     "ns-args: " + ns,
+                     "gs arities: " + gs.map(_.arity).mkString("\n"),
+                     "gs: " + gs.mkString(", ")
+                    )
+      throw new IllegalArgumentException(msg.mkString("\n"))
+    }
 
   override def arity = n
+  override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
 }
 
 // syntactic convenience
@@ -60,9 +70,18 @@
         g.eval(ns.init ::: List(ns.last - 1, r))
       }
     }
-    else throw new IllegalArgumentException("Pr: args")
+    else {
+      val msg = List("Pr f: " + f, 
+                     "g: " + g,
+                     "n: " + n,
+                     "f arity: " + f.arity,
+                     "g arity: " + g.arity,
+                     "ns-args: " + ns)
+      throw new IllegalArgumentException(msg.mkString("\n"))
+    }
 
   override def arity = n + 1
+  override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
 }
 
 // syntactic convenience
@@ -107,6 +126,7 @@
 val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1)))
 val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1)))
 val Disj = Sign o (Add o (Id(2, 0), Id(2, 1)))
+val Le = Disj o (Less, Eq)
 
 def Nargs(n: Int, m: Int) : List[Rec] = m match {
   case 0 => Nil
@@ -115,6 +135,7 @@
 
 def Sigma(f: Rec) = {
   val ar = f.arity
+  println("sigma f-ar: " + ar)
   Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))), 
      Add o (Id(ar + 1, ar), 
             Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1))))))
@@ -140,6 +161,8 @@
 //Definition on page 77 of Boolos's book.
 def Minr(f: Rec) = {
   val ar = f.arity
+  println("f-arity " + ar)
+  println("Nargs " + Nargs(ar + 1, ar - 1) + " and " + List(Id(ar + 1, ar)))
   Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar))))))
 }
 
@@ -147,7 +170,7 @@
 def Maxr(f: Rec) = {
   val ar  = f.arity
   val rt  = Id(ar + 1, ar - 1) 
-  val rf1 = Less o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) 
+  val rf1 = Le o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) 
   val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1)))) 
   val Qf  = Not o All(rt, Disj o (rf1, rf2)) 
   Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1)))
@@ -206,12 +229,12 @@
 }
 
 val Lg = {
- val rec_lgR = Less o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
- val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0)), 
-                             Less o (Const(1) o (Id(2, 0)), Id(2, 1))))
- val conR2 = Not o ConR1
+ val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
+ val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), 
+                     Less o (Const(1) o (Id(2, 0), Id(2, 1))))
+ val conR2 = Not o (conR1)
  Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), 
-        Mult o (conR2, Constn(0) o (Id(2, 0)))) 
+        Mult o (conR2, Const(0) o (Id(2, 0)))) 
 }