diff options
| -rw-r--r-- | huffman-encode.lisp | 40 |
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 |