summaryrefslogtreecommitdiff
path: root/lists
diff options
context:
space:
mode:
Diffstat (limited to 'lists')
-rw-r--r--lists/shuffle.lisp4
1 files 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)))