# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597893428 -32400
# Node ID e87ed47742b1d6e1a7722bd335c534dcb19fa680
# Parent  7b890eb577a6ef23b96b6cba1dd860218b9f84ab
...

diff -r 7b890eb577a6 -r e87ed47742b1 Symmetric.agda
--- a/Symmetric.agda	Thu Aug 20 09:44:08 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 12:17:08 2020 +0900
@@ -163,17 +163,22 @@
 plist {suc j} perm = plist1 j a<sa where
     n = suc j
     plist1 : (i : ℕ ) → i < n → List ℕ
-    plist1  zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
-    plist1  (suc i) (s≤s lt) = toℕ (  perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1  i (<-trans lt a<sa) 
+    plist1  zero _           = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
+    plist1  (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt)))         ∷ plist1  i (<-trans lt a<sa) 
 
 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
+test10 = plist (eperm {2} {0} ( s≤s z≤n)  pid)
+test11 = plist (eperm {2} {0} ( s≤s z≤n)  (eperm {1} {0} (s≤s z≤n) pid))
+test20 = plist (eperm {2} {1} (s≤s ( s≤s z≤n)) pid)
+test21 = plist (eperm {2} {1} (s≤s ( s≤s z≤n)) (eperm {1} {0} (s≤s z≤n) pid))
+test3 =  test10  ∷ test11 ∷ test20 ∷ test21 ∷ []
 
 NL : (n : ℕ ) → Set
 NL 0 = ℕ
 NL (suc n) = List ( NL n )
 
 pls : (n : ℕ ) → List (List ℕ )
-pls n = pls1 n n lem0  where
+pls n = Data.List.map plist (pls6 n) where
    lem0 : {n : ℕ } → n ≤ n
    lem0 {zero} = z≤n
    lem0 {suc n} = s≤s lem0
@@ -182,12 +187,12 @@
    lem1 (s≤s lt) = s≤s (lem1 lt)
    lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
    lem2 i≤n = ≤-trans i≤n ( refl-≤s )
-   pls3 :  ( i n : ℕ ) → (i<n : i < n ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n))
-   pls3 i n i<n [] x = x
-   pls3 i n i<n (h ∷ t) x = pls3 i n i<n t (  eperm {n} {i} i<n h ∷ x )
-   pls2 : ( i n : ℕ ) → (i<n : i ≤ n ) → List (Permutation (suc n) (suc n))
-   pls2 0 n i≤<n = pid ∷ []
-   pls2 (suc i) (suc n) (s≤s i≤n) = pls3 i (suc n) (lem1 i≤n) ( pls2 i n i≤n) []
-   pls1 : ( i n : ℕ ) → i ≤ n  → List (List ℕ) 
-   pls1 0 n _ = []
-   pls1 (suc i) n (s≤s i≤n) = (Data.List.map plist ( pls2 i n (lem2 i≤n)) ) ++ pls1 i n (lem2 i≤n)  
+   pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
+   pls4 zero n i≤n perm x = pid ∷ x
+   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {i} i≤n perm ∷ x)
+   pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
+   pls5 n [] x = x
+   pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
+   pls6 :  ( n : ℕ ) → List (Permutation (suc n) (suc n)) 
+   pls6 zero = pid ∷ []
+   pls6 (suc n) =  pls5 (suc n) (pls6 n) []