From 3e761c7bfce4be1f27e28b05d9378129c1484555 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 14 Jul 2022 17:30:08 +0900 Subject: huffman-encode: decode1-append-encode-1: Renamed. --- huffman-encode.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -- cgit v1.2.3