summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--huffman-encode.lisp36
1 files changed, 18 insertions, 18 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp
index ff9fc20..728b012 100644
--- a/huffman-encode.lisp
+++ b/huffman-encode.lisp
@@ -31,15 +31,6 @@
(equal (first x) 'leaf)
(rationalp (third x))))))
-(defun huffman-leaf (s w)
- (declare (xargs :guard (rationalp w)))
- (list 'leaf s w))
-
-(defun leaf-symbol (x)
- (declare (xargs :guard (and (huffman-treep x)
- (not (nodep x)))))
- (second x))
-
(defun symbol-list (x)
(declare (xargs :guard (huffman-treep x)))
(if (nodep x)
@@ -50,15 +41,14 @@
(declare (xargs :guard (huffman-treep x)))
(third x))
-(defun left (x)
- (declare (xargs :guard (and (huffman-treep x)
- (nodep x))))
- (fourth x))
+(defun huffman-leaf (s w)
+ (declare (xargs :guard (rationalp w)))
+ (list 'leaf s w))
-(defun right (x)
+(defun leaf-symbol (x)
(declare (xargs :guard (and (huffman-treep x)
- (nodep x))))
- (fifth x))
+ (not (nodep x)))))
+ (second x))
(defun huffman-node (l r)
(declare (xargs :guard (and (huffman-treep l)
@@ -70,7 +60,17 @@
l
r))
-(defthm huffman-leaf-elim
+(defun left (x)
+ (declare (xargs :guard (and (huffman-treep x)
+ (nodep x))))
+ (fourth x))
+
+(defun right (x)
+ (declare (xargs :guard (and (huffman-treep x)
+ (nodep x))))
+ (fifth x))
+
+(defthm leaf-symbol-weight-elim
(implies (and (not (nodep x))
(huffman-treep x))
(equal (huffman-leaf (leaf-symbol x)
@@ -88,7 +88,7 @@
(consp (cddddr x))
(null (cdr (cddddr x)))))))
-(defthm huffman-node-elim
+(defthm left-right-elim
(implies (and (nodep x)
(huffman-treep x))
(equal (huffman-node (left x) (right x))