huffman-encode: Rearrange functions and thiorems about node-count.

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