summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--huffman-encode.lisp19
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)))