diff options
| -rw-r--r-- | lists/perm.lisp | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp index 4668a2b..36253ec 100644 --- a/lists/perm.lisp +++ b/lists/perm.lisp @@ -34,6 +34,11 @@ :hints (("Goal" :induct (perm y x)))))) (local + (defthm member-remove1 + (implies (not (equal x y)) + (iff (member x (remove1 y z)) + (member x z))))) +(local (encapsulate () @@ -43,12 +48,6 @@ (remove1 y (remove1 x z))))) (local - (defthm member-remove1 - (implies (not (equal x y)) - (iff (member x (remove1 y z)) - (member x z))))) - - (local (defthm perm-remove1 (implies (perm x y) (perm (remove1 e x) |