From 3ebc1d21bf5fe94ada90a812bbc7879f7a21719f Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 16 Jul 2022 15:33:25 +0900
Subject: perm: Moved to lists directory.

---
 lists/perm.lisp | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 perm.lisp       | 67 ---------------------------------------------------------
 2 files changed, 67 insertions(+), 67 deletions(-)
 create mode 100644 lists/perm.lisp
 delete mode 100644 perm.lisp

diff --git a/lists/perm.lisp b/lists/perm.lisp
new file mode 100644
index 0000000..e1d8c77
--- /dev/null
+++ b/lists/perm.lisp
@@ -0,0 +1,67 @@
+(in-package "ACL2")
+
+(defun perm (x y)
+  (cond
+    ((atom x) (atom y))
+    ((member-equal (car x) y)
+     (perm (cdr x) (remove1-equal (car x) y)))
+    (t nil)))
+
+(local
+ (defthm perm-reflexive
+   (perm x x)))
+
+(local
+ (encapsulate
+   ()
+   (local
+    (defthm perm-member
+      (implies (and (consp y)
+                    (perm x y))
+               (member (car y) x))))
+
+   (local
+    (defthm perm-remove1
+      (implies (and (consp y) (perm x y))
+               (perm (remove1 (car y) x)
+                     (cdr y)))))
+
+   (defthm perm-symmetric
+     (implies (perm x y)
+              (perm y x))
+     :hints (("Goal" :induct (perm y x))))))
+
+(local
+ (encapsulate
+   ()
+
+   (local
+    (defthm remove1-remove1
+      (equal (remove1 x (remove1 y z))
+             (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)
+                     (remove1 e y)))))
+
+   (local
+    (defthm perm-not-member
+      (implies (and (member e x)
+                    (not (member e y)))
+               (not (perm x y)))
+      :hints (("Subgoal *1/3" :cases ((equal (car x) e))))))
+
+   (defthm perm-transitive
+     (implies (and (perm x y)
+                   (perm y z))
+              (perm x z)))))
+
+(defequiv perm)
diff --git a/perm.lisp b/perm.lisp
deleted file mode 100644
index e1d8c77..0000000
--- a/perm.lisp
+++ /dev/null
@@ -1,67 +0,0 @@
-(in-package "ACL2")
-
-(defun perm (x y)
-  (cond
-    ((atom x) (atom y))
-    ((member-equal (car x) y)
-     (perm (cdr x) (remove1-equal (car x) y)))
-    (t nil)))
-
-(local
- (defthm perm-reflexive
-   (perm x x)))
-
-(local
- (encapsulate
-   ()
-   (local
-    (defthm perm-member
-      (implies (and (consp y)
-                    (perm x y))
-               (member (car y) x))))
-
-   (local
-    (defthm perm-remove1
-      (implies (and (consp y) (perm x y))
-               (perm (remove1 (car y) x)
-                     (cdr y)))))
-
-   (defthm perm-symmetric
-     (implies (perm x y)
-              (perm y x))
-     :hints (("Goal" :induct (perm y x))))))
-
-(local
- (encapsulate
-   ()
-
-   (local
-    (defthm remove1-remove1
-      (equal (remove1 x (remove1 y z))
-             (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)
-                     (remove1 e y)))))
-
-   (local
-    (defthm perm-not-member
-      (implies (and (member e x)
-                    (not (member e y)))
-               (not (perm x y)))
-      :hints (("Subgoal *1/3" :cases ((equal (car x) e))))))
-
-   (defthm perm-transitive
-     (implies (and (perm x y)
-                   (perm y z))
-              (perm x z)))))
-
-(defequiv perm)
-- 
cgit v1.2.3