From a4331bbef99dc67fe30775d677d368a62810d9b4 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Mon, 18 Jul 2022 02:35:07 +0900
Subject: lists/shuffle: Solve Double-rewrite warning.

---
 lists/shuffle.lisp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lists/shuffle.lisp b/lists/shuffle.lisp
index 61d7e08..20787a4 100644
--- a/lists/shuffle.lisp
+++ b/lists/shuffle.lisp
@@ -32,7 +32,7 @@
    (implies (and (consp x)
                  (< i (len x)))
             (perm (remove-nth i x)
-                  (remove1 (nth i x) x)))
+                  (remove1 (nth i x) (double-rewrite x))))
    :hints (("Goal" :induct (remove-nth i x))
            ("Subgoal *1/3.8'"
             :cases ((consp (cdr x)))))))
@@ -44,4 +44,4 @@
             (member (nth i x) x))))
 
 (defthm perm-shuffle
-  (perm (mv-nth 0 (shuffle x state)) x))
+  (perm (mv-nth 0 (shuffle x state)) (double-rewrite x)))
-- 
cgit v1.2.3