From 05bb99b8f3f4f31699b945a01537f18e40f61bd8 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 14 Jul 2022 17:30:23 +0900 Subject: huffman-encode: Refactor. --- huffman-encode.lisp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'huffman-encode.lisp') diff --git a/huffman-encode.lisp b/huffman-encode.lisp index 44c122d..9cb44d5 100644 --- a/huffman-encode.lisp +++ b/huffman-encode.lisp @@ -346,7 +346,6 @@ (append (encode-1 (car x) tree) (encode (cdr x) tree)))) - (defun bit-listp (x) (declare (xargs :guard t)) (if (atom x) @@ -407,7 +406,7 @@ (nodep tree)) (< (len (mv-nth 1 (decode-1 x tree))) (len x)))) - + (defthm member-append (iff (member-equal e (append x y)) (or (member-equal e x) @@ -425,12 +424,12 @@ (implies (and (huffman-treep tree) (member-equal x (symbol-list tree))) (and (equal (mv-nth 0 (decode-1 (append (encode-1 x tree) - y) - tree)) + y) + tree)) x) (equal (mv-nth 1 (decode-1 (append (encode-1 x tree) - y) - tree)) + y) + tree)) y)))) (defthm decode-encode-to-decode1-encode1 @@ -439,11 +438,11 @@ (member-equal x (symbol-list tree)) (subsetp y (symbol-list tree))) (equal (decode (append (encode-1 x tree) - (encode y tree)) - tree) + (encode y tree)) + tree) (cons (mv-nth 0 (decode-1 (encode-1 x tree) tree)) (decode (encode y tree) - tree)))) + tree)))) :hints (("Goal" :induct (decode x tree)))) (defthm decode-encode @@ -452,5 +451,5 @@ (nodep tree) (subsetp x (symbol-list tree))) (equal (decode (encode x tree) - tree) + tree) x))) -- cgit v1.2.3