L-99: Solve P13 problem.

1 files changed, 51 insertions, 3 deletions

diff --git a/L-99.lisp b/L-99.lisp
index 5848ae9..15ae22f 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -343,13 +343,61 @@
            (equal (decode (encode-modified x))
                   x)))
 
+;; P13 (**) Run-length encoding of a list (direct solution).
+(defun encode-direct-1 (x prev n)
+  (cond
+    ((endp x)
+     (cond
+       ((zp n) nil)
+       ((equal n 1) (list prev))
+       (t (list (list n prev)))))
+    ((or (zp n)
+         (equal (car x) prev))
+     (encode-direct-1 (cdr x) (car x) (1+ n)))
+    ((equal n 1)
+     (cons prev (encode-direct-1 (cdr x) (car x) 1)))
+    (t  (cons (list n prev)
+              (encode-direct-1 (cdr x) (car x) 1)))))
+
+(defmacro encode-direct (x)
+  `(encode-direct-1 ,x nil 0))
+
+(defthm app-repeat-1
+  (implies (and (natp n)
+                (consp x))
+           (equal (app (repeat (car x) n) x)
+                  (cons (car x)
+                        (app (repeat (car x) n) (cdr x))))))
+
+(defthm decode-encode-direct-1
   (implies (and (atom-listp x)
                 (atom sym)
                 (natp n))
-           (equal (decode (encode-modified-1 x sym n))
+           (equal (decode (encode-direct-1 x sym n))
                   (app (repeat sym n) x))))
 
-(defthm decode-encode-mofified
+(defthm decode-encode-direct
   (implies (atom-listp x)
-           (equal (decode (encode-modified x))
+           (equal (decode (encode-direct x))
                   x)))
+
+(defthm not-zp-car-repeat
+  (implies (not (zp n))
+           (equal (car (repeat sym n)) sym)))
+
+(defthm consp-repeat
+  (implies (posp n)
+           (consp (repeat x n))))
+
+(defthm encode-direct-equal-encode-mofified-1
+  (implies (and (atom-listp x)
+                (atom sym)
+                (natp n))
+           (equal (encode-direct-1 x sym n)
+                  (encode-modified-1 (encode-1 (pack-1 x (repeat sym n)))))))
+
+(defthm encode-direct-equal-encode-mofified
+  (implies (atom-listp x)
+           (equal (encode-direct x)
+                  (encode-modified x))))
+