# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597975988 -32400
# Node ID a3ee2ca4f07d765658e1d972e67b1fc72130e2e1
# Parent  9ce6141ef479ddae091052aad757ea0ddedd00f9
...

diff -r 9ce6141ef479 -r a3ee2ca4f07d Symmetric.agda
--- a/Symmetric.agda	Thu Aug 20 21:59:22 2020 +0900
+++ b/Symmetric.agda	Fri Aug 21 11:13:08 2020 +0900
@@ -134,8 +134,19 @@
    pfill1 0 _ perm = perm
    pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )
 
-psawpim : {n m : ℕ} → 1 < m → m ≤ n → Permutation n n
-psawpim {n} {m} 1<m m≤n = pfill m≤n ( psawpn 1<m )
+psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n
+psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) )
+
+n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j
+n≤ (zero) {j} = z≤n
+n≤ (suc i) {j} = s≤s ( n≤ i )
+
+lem0 : {n : ℕ } → n ≤ n
+lem0 {zero} = z≤n
+lem0 {suc n} = s≤s lem0
+
+lem00 : {n m : ℕ } → n ≡ m → n ≤ m
+lem00 refl = lem0
 
 -- pconcat :  {n m : ℕ } → Permutation  m m → Permutation n n → Permutation (m + n)  (m + n) 
 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ?
@@ -144,22 +155,13 @@
 --    from n-1 length create n length inserting new element at position m
 
 eperm  : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
-eperm {0} {0} z≤n perm = pid
+eperm {0} {0} z≤n perm = pprep perm
 eperm {suc n} {0} z≤n perm = pprep perm
-eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3  (pprep perm) where
-    lemm3 : 2 + m ≤ suc n
-    lemm3 = s≤s (s≤s m<n)
-    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation (suc n)(suc n) → Permutation (suc n)(suc n)
-    eperm1 zero i i<ssm perm = perm ∘ₚ (psawpim {suc n} {i + m} {!!}  {!!} ) --- 1 < i + m , i + m ≤ suc (suc n)
-                                                                             -- m<n   : m ≤ n , i<ssm : i + zero ≤ suc (suc n)
-    eperm1 (suc m) i i<ssm perm = eperm1 m (suc i) (lemm4 i<ssm )  perm where
-       lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
-       lemm4 lt = begin
-          suc i + m  ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
-          suc m + i  ≡⟨ +-comm (suc m)  _  ⟩
-          i + suc m  ≤⟨ lt ⟩
-          suc n
-        ∎   where open  ≤-Reasoning
+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 (suc i) (s≤s si≤n) = eperm1 i (≤-trans si≤n refl-≤s )  ∘ₚ psawpim {suc n} {i}  (s≤s si≤n)
+
 
 plist  : {n  : ℕ} → Permutation n n → List ℕ
 plist {0} perm = []
@@ -169,28 +171,18 @@
     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) 
 
-testp = plist (psawpim {6} {4} (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))))
-testi00 = plist(pid {3}  )                                                           -- 0 ∷ 1 ∷ 2 ∷ []
-testi = plist (pid {3}  ∘ₚ psawpim {3} {2} (s≤s (s≤s z≤n))  (s≤s (s≤s z≤n)))         -- 0 ∷ 2 ∷ 1 ∷ []  -- 1 ∷ 0 ∷ 2 ∷ []
-testi0 = plist (pid {3}  ∘ₚ psawpim {3} {3} (s≤s (s≤s z≤n))  (s≤s ( s≤s (s≤s z≤n)))) -- 1 ∷ 0 ∷ 2 ∷ []  -- 1 ∷ 2 ∷ 0 ∷ []
+testi0 = plist   (pprep (pid {3}) )                                                          -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
+testi01 = plist  (psawpim {4} {2} (n≤ 4 {0}) )                                               -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ []
+testi02 = plist  (psawpim {4} {2} (n≤ 4 {0}) ∘ₚ psawpim {4} {1}  (n≤ 3))                     -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ []
+testi03 = plist ((psawpim (n≤  4 {0}) ∘ₚ psawpim  (n≤ 3) ) ∘ₚ psawpim {4} {0}  (n≤ 2 ))      -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []
+ttt0 =  testi0 ∷ testi01 ∷ testi02 ∷ testi03 ∷ []
 
-test0 = plist (eperm {1} {0} z≤n pid)
-test1 = plist (eperm {1} {1} (s≤s z≤n) pid)
-test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
-test11 = plist (eperm {2} {0} z≤n             (eperm {1} {0}  z≤n pid))
-test12 = plist (eperm {2} {0} z≤n             (eperm {1} {1}  (s≤s z≤n)  pid))
-test21 = plist (eperm {2} {1} (s≤s z≤n)       (eperm {1} {0}  z≤n pid))
-test22 = plist (eperm {2} {1} (s≤s z≤n)       (eperm {1} {1}  (s≤s z≤n)  pid))
-test23 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {0}  z≤n  pid))
-test24 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {1}  (s≤s z≤n)  pid))
-test3 =  test11  ∷ test12 ∷ test21 ∷ test22 ∷ test23 ∷ test24 ∷ []
-
-lem0 : {n : ℕ } → n ≤ n
-lem0 {zero} = z≤n
-lem0 {suc n} = s≤s lem0
-
-lem00 : {n m : ℕ } → n ≡ m → n ≤ m
-lem00 refl = lem0
+et0 = eperm (n≤ 4 ) (pid {4}) -- (4 ∷ 0 ∷ 1 ∷ 2 ∷ 3 ∷ [])
+et1 = eperm (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 ∷ [] 
 
 pls : (n : ℕ ) → List (List ℕ )
 pls n = Data.List.map plist (pls6 n) where
@@ -201,7 +193,7 @@
    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 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {i} (≤-trans refl-≤s i≤n ) 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
    pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)