# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598916460 -32400
# Node ID 92f3c9b926bd26a0927fb2cc67abcfddd14e335f
# Parent  0fa8a49dc38bb33bd1b36c0b470ca30b452e3d10
...

diff -r 0fa8a49dc38b -r 92f3c9b926bd Putil.agda
--- 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