L-99: Fix encode function.

1 files changed, 15 insertions, 1 deletions

diff --git a/L-99.lisp b/L-99.lisp
index a4e5a59..efd9e15 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -244,7 +244,7 @@
     ((endp x)
      (if (zp n)
          nil
-         (list (list prev n))))
+         (list (list n prev))))
     ((or (zp n)
          (equal (car x) prev))
      (encode-1 (cdr x) (car x) (1+ n)))
@@ -254,4 +254,18 @@
 (defmacro encode (x)
   `(encode-1 ,x nil 0))
 
+(defun sum-of-cars (x)
+  (if (endp x)
+      0
+      (+ (caar x)
+         (sum-of-cars (cdr x)))))
+
+(defthm sum-of-cars-encode-1
+  (implies (natp n)
+           (equal (sum-of-cars (encode-1 x sym n))
+                  (+ n (len x)))))
+
+(defthm sum-of-cars-encode
+  (equal (sum-of-cars (encode x))
+         (len x)))