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

diff -r bc289ffd0896 -r 7b890eb577a6 Symmetric.agda
--- a/Symmetric.agda	Thu Aug 20 09:07:54 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 09:44:08 2020 +0900
@@ -14,7 +14,7 @@
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 open import Data.Nat.Properties -- using (<-trans)
 open import Relation.Binary.PropositionalEquality 
-open import Data.List using (List; []; _∷_ ; length)
+open import Data.List using (List; []; _∷_ ; length ; _++_ )
 open import nat
 
 fid : {p : ℕ } → Fin p → Fin p
@@ -173,7 +173,7 @@
 NL (suc n) = List ( NL n )
 
 pls : (n : ℕ ) → List (List ℕ )
-pls n = pls1 n n lem0 where
+pls n = pls1 n n lem0  where
    lem0 : {n : ℕ } → n ≤ n
    lem0 {zero} = z≤n
    lem0 {suc n} = s≤s lem0
@@ -182,9 +182,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 )
-   pls2 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation (suc n) (suc n)
-   pls2 0 n i≤<n = pid 
-   pls2 (suc i) (suc n) (s≤s i≤n) = eperm {suc n} {i} (lem1 i≤n) ( pls2 i n i≤n)
-   pls1 : ( i n : ℕ ) → i ≤ n  → List (List ℕ)
+   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) = plist ( pls2 i n (lem2 i≤n)) ∷ pls1 i n (lem2 i≤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)