diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 17:30:08 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 17:30:08 +0900 |
| commit | 3e761c7bfce4be1f27e28b05d9378129c1484555 (patch) | |
| tree | c610e691a892e721cc81e419a48ac68a36bf71d3 /huffman-encode.lisp | |
| parent | a0e3ae6454cb363b70e8c07ce03689b690a6a5dc (diff) | |
huffman-encode: decode1-append-encode-1: Renamed.
Diffstat (limited to 'huffman-encode.lisp')
| -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) |