From 2a2010312569f19f8f789546eced8e3d1f2e8877 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 14 Jul 2022 13:05:14 +0900 Subject: huffman-encode: Rearrange functions and thiorems about node-count. --- huffman-encode.lisp | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'huffman-encode.lisp') 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 -- cgit v1.2.3