# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598233226 -32400
# Node ID 48926e810f5fb5f67d2c6befcf162ffd0944ac47
# Parent  afa989a4b7e991abf5bb33924217ca654ef00e8d
perm→FL done. pprep fix.

diff -r afa989a4b7e9 -r 48926e810f5f Putil.agda
--- a/Putil.agda	Sun Aug 23 20:39:35 2020 +0900
+++ b/Putil.agda	Mon Aug 24 10:40:26 2020 +0900
@@ -42,19 +42,19 @@
 pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
    p→ : Fin (suc n) → Fin (suc n)
    p→ zero = zero
-   p→ (suc x) = suc ( perm  ⟨$⟩ˡ x)
+   p→ (suc x) = suc ( perm  ⟨$⟩ʳ x)
 
    p← : Fin (suc n) → Fin (suc n)
    p← zero = zero
-   p← (suc x) = suc ( perm  ⟨$⟩ʳ x)
+   p← (suc x) = suc ( perm  ⟨$⟩ˡ x)
 
    piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x
    piso← zero = refl
-   piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) 
+   piso← (suc x) = cong (λ k → suc k ) (inverseʳ perm) 
 
    piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
    piso→ zero = refl
-   piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) 
+   piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) 
 
 pswap  : {n : ℕ }  → Permutation n n → Permutation (suc (suc n)) (suc (suc  n ))
 pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
@@ -273,39 +273,41 @@
 FL→perm f0 = pid
 FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
 
+t40 =                (# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) 
+t4 =  FL→perm ((# 2) :: t40 )
+
 t1 = plist (shrink (pid {3}  ∘ₚ (pins (n≤ 1))) refl)
-t3 = plist (pid {4} )
-    ∷ plist ( FL→perm ((# 0) :: ((# 0) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 1 ∷ 2 ∷ []) ∷
-    ∷ plist ( FL→perm ((# 1) :: ((# 0) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 2 ∷ 1 ∷ []) ∷
-    ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (1 ∷ 0 ∷ 2 ∷ []) ∷
-    ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (2 ∷ 0 ∷ 1 ∷ []) ∷
-    ∷ plist ( FL→perm ((# 1) :: ((# 2) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (1 ∷ 2 ∷ 0 ∷ []) ∷
-    ∷ plist ( FL→perm ((# 1) :: ((# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (2 ∷ 1 ∷ 0 ∷ []) ∷ 
-    ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))))
-    ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 1) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) ))
+t2 = plist ((pid {5} ) ∘ₚ transpose (# 2) (# 4)) ∷ plist (pid {5} ∘ₚ reverse )   ∷  []
+t3 = plist (FL→perm t40) -- ∷ plist (pprep (FL→perm t40))
+    -- ∷ plist ( pprep (FL→perm t40) ∘ₚ  pins ( n≤ 0 {3}  ))
+    -- ∷ plist ( pprep (FL→perm t40 )∘ₚ  pins ( n≤ 1 {2}  ))
+    -- ∷ plist ( pprep (FL→perm t40 )∘ₚ  pins ( n≤ 2 {1}  ))
+    -- ∷ plist ( pprep (FL→perm t40 )∘ₚ  pins ( n≤ 3 {0}  ))
+    ∷ plist ( FL→perm ((# 0) :: t40))  --  (0 ∷ 1 ∷ 2 ∷ []) ∷
+    ∷ plist ( FL→perm ((# 1) :: t40))  --  (0 ∷ 2 ∷ 1 ∷ []) ∷
+    ∷ plist ( FL→perm ((# 2) :: t40))  --  (1 ∷ 0 ∷ 2 ∷ []) ∷
+    ∷ plist ( FL→perm ((# 3) :: t40))  --  (2 ∷ 0 ∷ 1 ∷ []) ∷
+    -- ∷ plist ( FL→perm ((# 3) :: ((# 2) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (1 ∷ 2 ∷ 0 ∷ []) ∷
+    -- ∷ plist ( FL→perm ((# 3) :: ((# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (2 ∷ 1 ∷ 0 ∷ []) ∷ 
+    -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))))
+    -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) ))
     ∷ []
 
-t4 =  FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) )) 
--- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
-t5 = plist (flip t4)
-    ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] )
-    ∷ ( toℕ (t4 ⟨$⟩ʳ fromℕ≤ ( fin<n {_} {(t4 ⟨$⟩ˡ fromℕ≤ a<sa)})) ∷ [] )
-    ∷  plist (shrink ( t4  ∘ₚ flip (pins ( n≤  3 ) ) ) refl )
-    ∷  plist ( FL→perm (((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) 
-    ∷ []
- 
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
-perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 fl4 ) where
-    fl2 : Fin (suc n)
-    fl2 = perm ⟨$⟩ʳ fromℕ≤  (fin<n {suc n} {perm  ⟨$⟩ˡ fromℕ≤ a<sa} )
-    fl3 : toℕ fl2 < n
-    fl3 = {!!}
-    fl1 : Permutation (suc n) (suc n)
-    fl1 = perm ∘ₚ pinv ( pins fl3 )
-    fl4 : (fl1 ⟨$⟩ˡ fromℕ n) ≡ fromℕ n
-    fl4 = {!!}
+perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)  
+
+-- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
+t5 = plist (t4) ∷ plist (flip t4)
+    ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] )
+    ∷ ( toℕ (t4 ⟨$⟩ˡ (# 0)) ∷ [] )
+    -- ∷  plist ( t4  ∘ₚ flip (pins ( n≤  1 ) ))
+    ∷  plist (remove (# 0) t4  )
+    ∷  plist ( FL→perm t40 )
+    ∷ []
+ 
+t6 = perm→FL t4
 
 FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
 FL→iso f0 = refl