summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-14 13:05:14 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-14 13:05:14 +0900
commit2a2010312569f19f8f789546eced8e3d1f2e8877 (patch)
treede13a42edd1b6fb0bb50fa8ddd305489443a7cca
parentf3c662421bc7913604355012bcced5d75051e505 (diff)
huffman-encode: Rearrange functions and thiorems about node-count.
-rw-r--r--huffman-encode.lisp40
1 files changed, 20 insertions, 20 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp
index c8ca8b3..dc31b53 100644
--- a/huffman-encode.lisp
+++ b/huffman-encode.lisp
@@ -97,26 +97,6 @@
:in-theory (disable len=5)))
:rule-classes :elim)
-(defun node-count (x)
- (declare (xargs :guard (huffman-treep x)))
- (if (nodep x)
- (+ 1
- (node-count (left x))
- (node-count (right x)))
- 0))
-
-(defthm node-count-left
- (implies (nodep x)
- (< (node-count (left x))
- (node-count x)))
- :rule-classes :linear)
-
-(defthm node-count-right
- (implies (nodep x)
- (< (node-count (right x))
- (node-count x)))
- :rule-classes :linear)
-
(defthm huffman-treep-huffman-node
(implies (and (huffman-treep l)
(huffman-treep r))
@@ -173,6 +153,26 @@
(implies (rationalp w)
(huffman-treep (huffman-leaf s w))))
+(defun node-count (x)
+ (declare (xargs :guard (huffman-treep x)))
+ (if (nodep x)
+ (+ 1
+ (node-count (left x))
+ (node-count (right x)))
+ 0))
+
+(defthm node-count-left
+ (implies (nodep x)
+ (< (node-count (left x))
+ (node-count x)))
+ :rule-classes :linear)
+
+(defthm node-count-right
+ (implies (nodep x)
+ (< (node-count (right x))
+ (node-count x)))
+ :rule-classes :linear)
+
(in-theory (disable nodep huffman-treep
leaf-symbol
huffman-leaf huffman-node