summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-14 17:30:08 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-14 17:30:08 +0900
commit3e761c7bfce4be1f27e28b05d9378129c1484555 (patch)
treec610e691a892e721cc81e419a48ac68a36bf71d3
parenta0e3ae6454cb363b70e8c07ce03689b690a6a5dc (diff)
huffman-encode: decode1-append-encode-1: Renamed.
-rw-r--r--huffman-encode.lisp2
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)