diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:35:07 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:35:07 +0900 |
| commit | a4331bbef99dc67fe30775d677d368a62810d9b4 (patch) | |
| tree | 1b1983ff62b3655ff05ba89b99357a658cc751f5 | |
| parent | b22f11af26fe3108dbd9636b3e5c6973ab57e6dd (diff) | |
| -rw-r--r-- | lists/shuffle.lisp | 4 |
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))) |