diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 13:03:33 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-14 13:03:33 +0900 |
| commit | ef184a3fbfb0494d52d5c1993514cd8feed32233 (patch) | |
| tree | 8c38cf9ee28acea4c34bb77c8f8a45de79fde67b /huffman-encode.lisp | |
| parent | 07242a16ff73b043202a8e82a087e506ea7ad40b (diff) | |
huffman-encode: rationalp-weight/leaf: Fix.
Diffstat (limited to 'huffman-encode.lisp')
| -rw-r--r-- | huffman-encode.lisp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp index f634a84..8bdd05b 100644 --- a/huffman-encode.lisp +++ b/huffman-encode.lisp @@ -165,10 +165,9 @@ (implies (huffman-treep x) (rationalp (weight x)))) -(defthm rationalp-weight-2 - (implies (and (not (nodep (huffman-leaf lsl wt))) - (huffman-treep (huffman-leaf lsl wt))) - (rationalp wt))) +(defthm rationalp-weight/leaf + (implies (huffman-treep (huffman-leaf s w)) + (rationalp w))) (defthm huffman-treep-huffman-leaf (implies (rationalp w) |