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

diff -r 7c6f665e687f -r 933255f252ce src/Putil.agda
--- a/src/Putil.agda	Thu Sep 21 08:23:48 2023 +0900
+++ b/src/Putil.agda	Thu Sep 21 08:40:43 2023 +0900
@@ -508,39 +508,19 @@
       ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh1 perm p0=0 b)
       ... | tri> ¬a₁ ¬b₁ c₁ = ? where
            open ≡-Reasoning 
-           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 : {n : ℕ } → (y : Fin (suc n)) → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
            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 = ?
+           p15 : toℕ (Inverse.to perm (suc y)) ∸ 1 ≡ toℕ x
+           p15 = begin
+              toℕ (Inverse.to perm (suc y)) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm (suc k))  ∸ 1   ) (sym px=y) ⟩
+              toℕ (Inverse.to perm (suc (fromℕ< (p01 x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm k)  ∸ 1) (p11 _ (p01 x c) ) ⟩
+              toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseʳ perm) ⟩
+              toℕ (suc x) ∸ 1  ≡⟨ ? ⟩
+              toℕ x ∎
            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ℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁)  ≡⟨ lemma10 p15 ⟩
              fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎