# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695252228 -32400
# Node ID 7c6f665e687f5777db0dd32f9664201fb41c4829
# Parent  8fb16f9a882aefe94064d86a300b15c2c9167980
...

diff -r 8fb16f9a882a -r 7c6f665e687f src/Putil.agda
--- a/src/Putil.agda	Tue Sep 19 11:11:38 2023 +0900
+++ b/src/Putil.agda	Thu Sep 21 08:23:48 2023 +0900
@@ -502,14 +502,47 @@
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
    piso← x = p02 _ _ refl refl  where
       p02 : (y z : Fin n) → p← x ≡ y → p→ y ≡ z → z ≡ x
-      p02 y z px=y py=z with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0)
+      p02 y z px=y py=z with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0) 
       ... | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
-      ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ʳ (suc y)) (# 0)
+      ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ʳ (suc y)) (# 0) 
       ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh1 perm p0=0 b)
       ... | tri> ¬a₁ ¬b₁ c₁ = ? where
            open ≡-Reasoning 
-           p03 : toℕ (Inverse.to perm (suc x)) ≡ suc (toℕ y)
-           p03 = ?
+           p06 : fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c) ≡ y
+           p06 = px=y
+           p07 : fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁) ≡ z
+           p07 = py=z
+           p03 : toℕ (Inverse.from perm (suc x)) ≡ suc (toℕ y)
+           p03 = begin 
+              toℕ (Inverse.from perm (suc x))  ≡⟨ ? ⟩
+              suc (toℕ y) ∎ 
+           p04 : toℕ (Inverse.to perm (suc y)) ≡ suc (toℕ z)
+           p04 = ?
+           p05 : Inverse.to perm ( Inverse.from perm (suc x) ) ≡ suc x
+           p05 = inverseʳ perm  
+           p09 : Data.Nat.pred (toℕ (Inverse.to perm (suc (fromℕ< (p01 x c))))) < n
+           p09 = ? 
+           p11 : Data.Nat.pred (toℕ (Inverse.to perm (Inverse.from perm (suc x)))) < n
+           p11 = ?
+           p12 : toℕ (Inverse.to perm (suc (fromℕ< (p01 x c)))) ∸ 1 ≡ toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1
+           p12 = ?
+           p13 : Data.Nat.pred (suc (toℕ x)) < n
+           p13 = ?
+           p10 : Data.Nat.pred (toℕ (Inverse.to perm (suc y))) ≡ Data.Nat.pred (toℕ (Inverse.to perm (suc (fromℕ< (p01 x c))))) 
+           p10 = cong (λ k → Data.Nat.pred (toℕ (Inverse.to perm (suc k)))) (sym px=y)
+           p14 : toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1 ≡ toℕ x
+           p14 = ?
+           p08 : z ≡ x
+           p08 = begin
+             z ≡⟨ sym (py=z) ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁)  
+                ≡⟨ lemma10 p10 ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm 
+                (suc (fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c))))) } p09  ≡⟨ lemma10 p12 ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (Inverse.from perm (suc x))) ) } p11  ≡⟨ lemma10 ? ⟩
+             fromℕ< {Data.Nat.pred (toℕ (suc x) ) } p13  ≡⟨ lemma10 refl  ⟩
+             fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
+             x ∎  
 
         -- with perm ⟨$⟩ˡ (suc x) in eq 
         -- ... | t = ?