diff options
| -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))) |