diff options
| -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))) |