Mercurial > hg > Members > kono > Proof > galois

changeset 108:d9cd155310e5

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 Tue, 01 Sep 2020 19:03:21 +0900
parents 7e63fb16dc64
children 5d60a060453c
files Putil.agda
diffstat 1 files changed, 6 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Sep 01 18:56:10 2020 +0900
+++ b/Putil.agda	Tue Sep 01 19:03:21 2020 +0900
@@ -517,8 +517,12 @@
 shrink-iso {n} {perm} = record { peq = λ q → refl  } 
 
 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
-   → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= pid
-shrink-iso2 = {!!}
+   → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= perm
+shrink-iso2 {n} {perm} p=0 = record { peq =  s001 } where
+    s001 : (q : Fin (suc n)) → (pprep (shrink perm p=0) ⟨$⟩ʳ q) ≡ (perm ⟨$⟩ʳ q)
+    s001 zero = {!!}
+    s001 (suc q) = {!!}
+
 
 shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)}
     → x =p= y