diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 17:29:36 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 17:29:36 +0900 |
| commit | a0e3ae6454cb363b70e8c07ce03689b690a6a5dc (patch) | |
| tree | e4dbb4c1b83af940c8477885d580100306bf7196 | |
| parent | 112364796296fd0721674f271d27d5e2ae904ce8 (diff) | |
huffman-encode: consp-encode-1, consp-encode: Fix hypotheses.
| -rw-r--r-- | huffman-encode.lisp | 6 |
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)))) |