diff options
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) |