huffman-encode: Rearrance functions.

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