# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598170954 -32400
# Node ID 8224694a4ddaa88b24072a585211b39c4ce34cb8
# Parent  2283d6f8a2fbc70cd3ab5c71839a33a9296e074b
...

diff -r 2283d6f8a2fb -r 8224694a4dda Putil.agda
--- a/Putil.agda	Sun Aug 23 16:34:19 2020 +0900
+++ b/Putil.agda	Sun Aug 23 17:22:34 2020 +0900
@@ -133,17 +133,56 @@
 open import logic 
 
 shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (fromℕ n) ≡ fromℕ n → Permutation n n
-shrink {n} perm p0=0  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+shrink {n} perm pn=n  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+
+   sh3 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ˡ (fin+1 x)) ≡  n )
+   sh3 x eq = ⊥-elim ( nat-≡< sh31 fin<n ) where
+       sh31 : toℕ x ≡ n
+       sh31 = begin
+           toℕ x 
+        ≡⟨ {!!}  ⟩
+            toℕ (fin+1 x)
+        ≡⟨ cong (λ k → toℕ k ) (sym ( inverseʳ perm))  ⟩
+            toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fin+1 x)))
+        ≡⟨ {!!}  ⟩
+            toℕ (perm ⟨$⟩ʳ fromℕ n)
+        ≡⟨ cong ( λ k → toℕ (perm ⟨$⟩ʳ k )) (sym pn=n) ⟩
+            toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fromℕ n) ))
+        ≡⟨ cong (λ k → toℕ k ) ( inverseʳ perm ) ⟩
+            toℕ (fromℕ n)
+        ≡⟨ {!!}  ⟩
+            n 
+        ∎ where 
+        open ≡-Reasoning
+
+   sh4 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ʳ (fin+1 x)) ≡  n )
+   sh4 x eq = ⊥-elim ( nat-≡< sh41 fin<n ) where
+       sh41 : toℕ x ≡ n
+       sh41 = begin
+            toℕ x
+        ≡⟨ {!!}  ⟩
+            toℕ (fin+1 x)
+        ≡⟨ cong (λ k → toℕ k ) (sym ( inverseˡ perm))  ⟩
+            toℕ (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (fin+1 x)))
+        ≡⟨ {!!}  ⟩
+            toℕ ((perm ⟨$⟩ˡ fromℕ n))
+        ≡⟨ cong (λ k → toℕ k) pn=n ⟩
+            toℕ (fromℕ n)
+        ≡⟨ {!!}  ⟩
+            n 
+        ∎ where 
+        open ≡-Reasoning
+
    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 = {!!}
+   shlem→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b )
    shlem→ x | tri> ¬a ¬b 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 = {!!}
+   shlem← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b )
    shlem← x | tri> ¬a ¬b c = {!!}
 
    p→ : (x : Fin n ) →  Fin n 
@@ -182,7 +221,7 @@
           ∎ 
    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 = {!!}
+   piso← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b )
    piso← x | tri> ¬a ¬b c = {!!}
 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
@@ -210,7 +249,7 @@
           ∎ 
    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 = {!!}
+   piso→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b )
    piso→ x | tri> ¬a ¬b c = {!!}
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n