diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:28:20 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:28:20 +0900 |
| commit | 9278fc03885110fed1ecc4fa895b73443e224816 (patch) | |
| tree | 34cfa959b4bf501b3a411c785c4cc9ac6b32b7bd | |
| parent | 87f47e7a248325933d2aa269de898ef521716650 (diff) | |
lists/perm: FIx perm-rev theorem.
| -rw-r--r-- | lists/perm.lisp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp index d93a0c5..2fcff12 100644 --- a/lists/perm.lisp +++ b/lists/perm.lisp @@ -74,8 +74,18 @@ (local (include-book "std/lists/rev" :dir :system)) + +(local + (encapsulate + () + (local (defthm perm-rev + (perm (rev x) (double-rewrite x)) + :hints (("Goal" :induct (perm x x))))) + + (defcong perm perm (rev x) 1))) + (local (defthm perm-rev - (perm (rev x) (double-rewrite x)) + (perm (rev x) x) :hints (("Goal" :induct (perm x x))))) (defcong perm perm (append x y) 2) |