diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:12:25 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:12:25 +0900 |
| commit | a03cb62c324489dc4c41f84bace7e53e1d6b0efb (patch) | |
| tree | 3e0ee1bafe0da32f161ecb973f00eee5acc0b6a6 | |
| parent | f23d7365a67c9b73a767162b728ed3fbdb3b79ac (diff) | |
lists/perm: Move member-remove1.
| -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) |