# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597983207 -32400
# Node ID 88f9aff7eb71282f47c501701ae00a24d204cef6
# Parent  a3ee2ca4f07d765658e1d972e67b1fc72130e2e1
eperm done?

diff -r a3ee2ca4f07d -r 88f9aff7eb71 Symmetric.agda
--- a/Symmetric.agda	Fri Aug 21 11:13:08 2020 +0900
+++ b/Symmetric.agda	Fri Aug 21 13:13:27 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 ; _++_ ) renaming (reverse to rev )
+open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ) renaming (reverse to rev )
 open import nat
 
 fid : {p : ℕ } → Fin p → Fin p
@@ -159,7 +159,7 @@
 eperm {suc n} {0} z≤n perm = pprep perm
 eperm {n} {suc m} (s≤s m<n) perm = eperm1 (suc m) (≤-trans (s≤s (s≤s m<n)) lem0 ) where
     eperm1 : (i : ℕ ) → suc i ≤ suc n  → Permutation (suc n)(suc n) 
-    eperm1 zero (s≤s z≤n) = pid
+    eperm1 zero (s≤s z≤n) = pprep perm
     eperm1 (suc i) (s≤s si≤n) = eperm1 i (≤-trans si≤n refl-≤s )  ∘ₚ psawpim {suc n} {i}  (s≤s si≤n)
 
 
@@ -177,12 +177,13 @@
 testi03 = plist ((psawpim (n≤  4 {0}) ∘ₚ psawpim  (n≤ 3) ) ∘ₚ psawpim {4} {0}  (n≤ 2 ))      -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []
 ttt0 =  testi0 ∷ testi01 ∷ testi02 ∷ testi03 ∷ []
 
-et0 = eperm (n≤ 4 ) (pid {4}) -- (4 ∷ 0 ∷ 1 ∷ 2 ∷ 3 ∷ [])
-et1 = eperm (n≤ 3 ) (pid {4}) -- (0 ∷ 4 ∷ 1 ∷ 2 ∷ 3 ∷ [])
+et0 = eperm {4} {4} (n≤ 4 ) (pid {4}) -- (4 ∷ 0 ∷ 1 ∷ 2 ∷ 3 ∷ [])
+et1 = eperm {4} {3} (n≤ 3 ) (pid {4}) -- (0 ∷ 4 ∷ 1 ∷ 2 ∷ 3 ∷ [])
 et2 = eperm (n≤ 2 ) (pid {4}) -- (0 ∷ 1 ∷ 4 ∷ 2 ∷ 3 ∷ [])
 et3 = eperm (n≤ 1 ) (pid {4}) -- (0 ∷ 1 ∷ 2 ∷ 4 ∷ 3 ∷ [])
 et4 = eperm (n≤ 0 ) (pid {4}) -- (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
-ttt2 = plist et0 ∷ plist et1 ∷ plist et2 ∷  plist et3 ∷ plist et4 ∷ [] 
+et5 = eperm (n≤ 4 ) (eperm (n≤ 2) (pid {3})) -- (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
+ttt2 = plist et0 ∷ plist et1 ∷ plist et2 ∷  plist et3 ∷ plist et5 ∷ [] 
 
 pls : (n : ℕ ) → List (List ℕ )
 pls n = Data.List.map plist (pls6 n) where
@@ -192,7 +193,7 @@
    lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
    lem2 i≤n = ≤-trans i≤n ( refl-≤s )
    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 zero n i≤n perm x = pprep perm ∷ x
    pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {suc 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
@@ -200,3 +201,5 @@
    pls6 :  ( n : ℕ ) → List (Permutation (suc n) (suc n)) 
    pls6 zero = pid ∷ []
    pls6 (suc n) =  pls5 (suc n) (pls6 n) []
+   pls7 : List (List ℕ )
+   pls7 = Data.List.map plist (pls4 2 2 lem0 (eperm (n≤ 0 ) (pid {1})) (pls4 2 2 lem0 (eperm (n≤ 1 ) (pid {1})) [] ))