From 705f1d5c6d5ee8d1f3f84dfc9079801bec49b2b6 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 25 Jul 2021 10:44:16 +0900 Subject: L-99: Solve P13 problem. --- L-99.lisp | 54 +++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file 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)))) + -- cgit v1.2.3