Mercurial > hg > Members > kono > Proof > galois

changeset 101:92f3c9b926bd

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 08:27:40 +0900
parents 0fa8a49dc38b
children 00a711f99096
files Putil.agda
diffstat 1 files changed, 11 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 31 15:25:45 2020 +0900
+++ b/Putil.agda	Tue Sep 01 08:27:40 2020 +0900
@@ -294,6 +294,14 @@
                 (perm ⟨$⟩ʳ (# 0))
              ∎ )
 
+px=x : {n : ℕ }  → (x : Fin (suc n)) → pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x
+px=x {n} zero = refl
+px=x {suc n} (suc x) = p001 (# 0) x refl where
+     pprev : {!!} -- pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x
+     pprev = px=x x
+     p001 : (x m : Fin (suc n))  → x ≡ # 0  → (pins (toℕ≤pred[n] (suc m)) ⟨$⟩ʳ x) ≡ (suc m)
+     p001 x m eq = {!!}
+
 
 -- pp : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) →  Fin (suc n)
 -- pp  perm → (( perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0))
@@ -585,7 +593,9 @@
     f001 : perm ⟨$⟩ʳ (# 0) ≡ x
     f001 = begin
        (pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )) ⟨$⟩ʳ (# 0) 
-     ≡⟨ {!!}  ⟩
+     ≡⟨⟩
+       pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) 
+     ≡⟨ px=x x ⟩
        x 
      ∎
     x=0 :  (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ˡ (# 0) ≡ # 0