From ef184a3fbfb0494d52d5c1993514cd8feed32233 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 14 Jul 2022 13:03:33 +0900 Subject: huffman-encode: rationalp-weight/leaf: Fix. --- huffman-encode.lisp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'huffman-encode.lisp') 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) -- cgit v1.2.3