summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-14 17:29:36 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-14 17:29:36 +0900
commita0e3ae6454cb363b70e8c07ce03689b690a6a5dc (patch)
treee4dbb4c1b83af940c8477885d580100306bf7196
parent112364796296fd0721674f271d27d5e2ae904ce8 (diff)
huffman-encode: consp-encode-1, consp-encode: Fix hypotheses.
-rw-r--r--huffman-encode.lisp6
1 files changed, 2 insertions, 4 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp
index 6da268f..a1a0a21 100644
--- a/huffman-encode.lisp
+++ b/huffman-encode.lisp
@@ -390,8 +390,7 @@
(consp y))))
(defthm consp-encode-1
- (implies (and (member-equal x (symbol-list tree))
- (huffman-treep tree)
+ (implies (and (huffman-treep tree)
(nodep tree))
(consp (encode-1 x tree))))
@@ -399,8 +398,7 @@
(implies (and (consp x)
(true-listp x)
(huffman-treep tree)
- (nodep tree)
- (subsetp x (symbol-list tree)))
+ (nodep tree))
(consp (encode x tree))))