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