summaryrefslogtreecommitdiff
path: root/lists
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:28:20 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:28:20 +0900
commit9278fc03885110fed1ecc4fa895b73443e224816 (patch)
tree34cfa959b4bf501b3a411c785c4cc9ac6b32b7bd /lists
parent87f47e7a248325933d2aa269de898ef521716650 (diff)
lists/perm: FIx perm-rev theorem.
Diffstat (limited to 'lists')
-rw-r--r--lists/perm.lisp12
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)