Mercurial > hg > Members > kono > Proof > galois

changeset 36:ee56e29a903c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Aug 2020 23:31:48 +0900
parents 0364ad4f2a47
children 32db08b3c1a3
files Symmetric.agda
diffstat 1 files changed, 3 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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