# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598178188 -32400
# Node ID 518d364a58a37e2b8590a55c0b85a3d8ef6bb21b
# Parent  e26f784cd6b16e15be55e0ee2e8d9e20a309843b
shrink worked

diff -r e26f784cd6b1 -r 518d364a58a3 Putil.agda
--- a/Putil.agda	Sun Aug 23 18:07:18 2020 +0900
+++ b/Putil.agda	Sun Aug 23 19:23:08 2020 +0900
@@ -174,17 +174,23 @@
         ∎ where 
         open ≡-Reasoning
 
+   sh5 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ˡ (fin+1 x)) >  n )
+   sh5 x lt = ⊥-elim ( nat-≤> lt (fin<n {suc n} {perm ⟨$⟩ˡ (fin+1 x)}))
+
+   sh6 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ʳ (fin+1 x)) >  n )
+   sh6 x lt = ⊥-elim ( nat-≤> lt (fin<n {suc n} {perm ⟨$⟩ʳ (fin+1 x)}))
+
    shlem→ : (x : Fin n ) → toℕ (perm ⟨$⟩ˡ (fin+1 x))  < n 
    shlem→ x with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 x)))  n
    shlem→ x | tri< a ¬b ¬c = a
    shlem→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b )
-   shlem→ x | tri> ¬a ¬b c = {!!}
+   shlem→ x | tri> ¬a ¬b c = ⊥-elim ( sh5 x c )
 
    shlem← : (x : Fin n) → toℕ (perm ⟨$⟩ʳ (fin+1 x))  < n 
    shlem← x with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x)))  n
    shlem← x | tri< a ¬b ¬c = a
    shlem← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b )
-   shlem← x | tri> ¬a ¬b c = {!!}
+   shlem← x | tri> ¬a ¬b c = ⊥-elim ( sh6 x c )
 
    p→ : (x : Fin n ) →  Fin n 
    p→ x  = fromℕ≤ (shlem→ x)
@@ -220,10 +226,10 @@
           ≡⟨ fin+1-toℕ ⟩ 
              toℕ  x
           ∎ 
-   piso← x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
-   piso← x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
+   piso← x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( sh3 (fromℕ≤ a) b )
+   piso← x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c =  ⊥-elim ( sh5 _ c )
    piso← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b )
-   piso← x | tri> ¬a ¬b c = {!!}
+   piso← x | tri> ¬a ¬b c = ⊥-elim ( sh6 x c )
 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
    piso→ x with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 x)))  n
@@ -248,10 +254,25 @@
           ≡⟨ fin+1-toℕ ⟩ 
              toℕ  x
           ∎ 
-   piso→ x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
-   piso→ x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
+   piso→ x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( sh4 (fromℕ≤ a) b )
+   piso→ x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c =  ⊥-elim ( sh6 _ c )
    piso→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b )
-   piso→ x | tri> ¬a ¬b c = {!!}
+   piso→ x | tri> ¬a ¬b c = ⊥-elim ( sh5 x c )
+
+FL→perm   : {n : ℕ }  → FL n → Permutation n n 
+FL→perm f0 = pid
+FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
+
+t1 = plist (shrink (pid {3}  ∘ₚ (pins (n≤ 1))) refl)
+t3 =  plist ( FL→perm ((# 1) :: ((# 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 )) )))) ))
+    ∷ []
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
@@ -261,10 +282,6 @@
     fl1=pprep : perm =p= pprep ( shrink fl1 {!!} )
     fl1=pprep = {!!}
 
-FL→perm   : {n : ℕ }  → FL n → Permutation n n 
-FL→perm f0 = pid
-FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
-
 FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
 FL→iso f0 = refl
 FL→iso (x :: fl) = {!!} --with FL→iso fl