diff options
| -rw-r--r-- | huffman-encode.lisp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp index a1a0a21..44c122d 100644 --- a/huffman-encode.lisp +++ b/huffman-encode.lisp @@ -421,7 +421,7 @@ (equal (mv-nth 1 (decode-1 (encode-1 x tree) tree)) nil)))) -(defthm decode1-append +(defthm decode1-append-encode-1 (implies (and (huffman-treep tree) (member-equal x (symbol-list tree))) (and (equal (mv-nth 0 (decode-1 (append (encode-1 x tree) |