From 8974e4b43e59ab7fadc803009cc9dff9d283f36d Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 15 Jul 2022 22:16:32 +0900
Subject: huffman-encode: rationalp-0-count-and-remove: Use `mv-nth` function.

---
 huffman-encode.lisp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'huffman-encode.lisp')

diff --git a/huffman-encode.lisp b/huffman-encode.lisp
index 9cb44d5..febf07b 100644
--- a/huffman-encode.lisp
+++ b/huffman-encode.lisp
@@ -1,6 +1,8 @@
 ;;; Provide Huffman encoding
 (in-package "ACL2")
 
+(local (include-book "tools/mv-nth" :dir :system))
+
 ;;; Deine huffman tree
 (defun nodep (x)
   (declare (xargs :guard t))
@@ -321,7 +323,7 @@
               (message-to-pairs rest)))))
 
 (defthm rationalp-0-count-and-remove
-  (rationalp (car (count-and-remove e x))))
+  (rationalp (mv-nth 0 (count-and-remove e x))))
 
 (defthm symbol-weight-pair-listp-message-to-pairs
   (symbol-weight-pair-listp (message-to-pairs x)))
-- 
cgit v1.2.3