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