# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597847508 -32400
# Node ID ee56e29a903cc3f763ddfc7f4b3f26dfa9e523cd
# Parent  0364ad4f2a4779d98ccb9c0ffdbc16f29bd8b73d
...

diff -r 0364ad4f2a47 -r ee56e29a903c Symmetric.agda
--- a/Symmetric.agda	Wed Aug 19 23:23:07 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 23:31:48 2020 +0900
@@ -135,8 +135,8 @@
 eperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
 eperm {zero} ()
 eperm {n} {0} (s≤s z≤n) perm = pprep perm
-eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 {!!} (pswap {0} pid ) (pprep perm) where
-    eperm1 : (m i : ℕ ) → i < suc (suc m)  → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n)
-    eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill {!!} sw )
+eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 (s≤s (s≤s (z≤n)))  (pswap {0} pid ) (pprep perm) where
+    eperm1 : (m i : ℕ ) → i ≤ suc (suc m)  → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n)
+    eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill {!!} sw )  -- i ≤ suc (suc n)
     eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) {!!} (pprep sw) perm