From a0e3ae6454cb363b70e8c07ce03689b690a6a5dc Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 14 Jul 2022 17:29:36 +0900 Subject: huffman-encode: consp-encode-1, consp-encode: Fix hypotheses. --- huffman-encode.lisp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'huffman-encode.lisp') 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)))) -- cgit v1.2.3