diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 17:30:23 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 17:30:47 +0900 |
| commit | 05bb99b8f3f4f31699b945a01537f18e40f61bd8 (patch) | |
| tree | 27e0c68866dd949f8103631279b179bf0c9f867c /huffman-encode.lisp | |
| parent | 3e761c7bfce4be1f27e28b05d9378129c1484555 (diff) | |
huffman-encode: Refactor.
Diffstat (limited to 'huffman-encode.lisp')
| -rw-r--r-- | huffman-encode.lisp | 19 |
1 files changed, 9 insertions, 10 deletions
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))) |