summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-14 13:03:33 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-14 13:03:33 +0900
commitef184a3fbfb0494d52d5c1993514cd8feed32233 (patch)
tree8c38cf9ee28acea4c34bb77c8f8a45de79fde67b
parent07242a16ff73b043202a8e82a087e506ea7ad40b (diff)
huffman-encode: rationalp-weight/leaf: Fix.
-rw-r--r--huffman-encode.lisp7
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)