# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598161415 -32400
# Node ID 3e677c24a6cc9140c8bc9e5a75c1bbb38979e4bd
# Parent  ddec1ef4f5e4db48c5fc31800cee9cf27c2d5843
...

diff -r ddec1ef4f5e4 -r 3e677c24a6cc Putil.agda
--- a/Putil.agda	Sun Aug 23 13:39:14 2020 +0900
+++ b/Putil.agda	Sun Aug 23 14:43:35 2020 +0900
@@ -132,66 +132,37 @@
 
 open import logic 
 
-shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
+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
-   shlem→ : (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
-   shlem→ x px=0 = begin
-          x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
-          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x)           ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) px=0 ⟩
-          perm ⟨$⟩ʳ zero                     ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) (sym p0=0) ⟩
-          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero)        ≡⟨ inverseʳ perm  ⟩
-          zero
-       ∎ 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 = {!!}
 
-   shlem← : (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero
-   shlem← x px=0 =  begin
-          x                                  ≡⟨ sym (inverseˡ perm ) ⟩
-          perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x )          ≡⟨ cong (λ k →  perm ⟨$⟩ˡ k ) px=0 ⟩
-          perm ⟨$⟩ˡ zero                     ≡⟨ p0=0  ⟩
-          zero
-       ∎ 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 = {!!}
 
-   sh2 : {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero
-   sh2 {x} eq with shlem→ (suc x) eq
-   sh2 {x} eq | ()
-
-   p→ : Fin n → Fin n 
-   p→ x = fin-1 ( perm ⟨$⟩ˡ (suc x) ) sh2
-
-   ssh4 : (x : Fin n  ) → suc (p→  x) ≡ perm ⟨$⟩ˡ (suc x)
-   ssh4 = {!!}
-
-   sh1 : {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero
-   sh1 {x} eq with shlem← (suc x) eq
-   sh1 {x} eq | ()
+   p→ : (x : Fin n ) →  Fin n 
+   p→ x  = fromℕ≤ (shlem→ x)
 
    p← : Fin n → Fin n 
-   p← x = fin-1 ( perm ⟨$⟩ʳ (suc x) ) sh1 
+   p← x  = fromℕ≤ (shlem← x)
 
--- fin-1-sx
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
-   piso← x = sh3 where
-      sh3 :  fin-1 ( perm ⟨$⟩ˡ (suc (  fin-1 ( perm ⟨$⟩ʳ (suc x)  ) sh1 ))) sh2 ≡ x
-      sh3 =  begin
-          fin-1 ( perm ⟨$⟩ˡ (suc (  fin-1 ( perm ⟨$⟩ʳ (suc x)  ) sh1 ))) sh2
-           ≡⟨ cong (λ k → fin-1 (perm ⟨$⟩ˡ k ) (sh4 k) ) (fin-1-xs _ sh5 ) ⟩
-          fin-1 ( perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ (suc x)  )) sh6 ≡⟨ cong (λ k → fin-1 k {!!} ) (inverseˡ perm) ⟩
-          fin-1 (suc x) (λ ()) ≡⟨ fin-1-sx x ⟩
-          x
-       ∎ where
-           open ≡-Reasoning
-           sh4 : (k : Fin (suc n)) → ¬ Inverse.from perm Π.⟨$⟩ k ≡ zero
-           sh4 = {!!}
-           sh5  : ¬ Inverse.to perm Π.⟨$⟩ suc x ≡ zero
-           sh5 = {!!}
-           sh6  : ¬ Inverse.from perm Π.⟨$⟩ (Inverse.to perm Π.⟨$⟩ suc x) ≡ zero
-           sh6 = {!!}
-
+   piso← x with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x)))  n
+   piso← x | tri< a ¬b ¬c with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x)))  n
+   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 = {!!}
+   piso← x | tri≈ ¬a b ¬c = {!!}
+   piso← x | tri> ¬a ¬b c = {!!}
 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
-   piso→ x = sh4 where
-      sh4 :  fin-1 ( perm ⟨$⟩ʳ (suc (  fin-1 ( perm ⟨$⟩ˡ (suc x)  ) sh2 ))) sh1 ≡ x
-      sh4 = {!!}
+   piso→ x = {!!}
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0