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

diff -r 3e14418230bc -r db8229569750 src/bijection.agda
--- a/src/bijection.agda	Sun Jun 18 20:17:50 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 07:11:04 2023 +0900
@@ -931,20 +931,59 @@
              ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ j≤i a<sa  ))
              lem02 (suc j) (s≤s j≤i) | tri> ¬a ¬b c₁ = lem02 j (≤-trans j≤i a≤sa)
          lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
-    c1<count-A zero (suc i) = ?
+    c1<count-A zero (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
+    ... | no nisa | tri< a ¬b ¬c = ?
+    ... | no nisa | tri≈ ¬a b ¬c = ?
+    ... | no nisa | tri> ¬a ¬b c₁ = ? where
+          lem10 : c1 zero i ≤ count-A i
+          lem10 = c1<count-A 0 i
+    ... | yes isa | s = ?
     c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
     ... | no nisa | tri< a ¬b ¬c = ? where -- subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
           lem13 : c1 n i ≡ c1 n (suc i) 
           lem13 = c1+0 {n} {i} nisa
           lem10 : c1 n i ≤ count-A i
           lem10 = c1<count-A n i
+          lem14 : count-A (suc i) ≡ suc (count-A i)
+          lem14 = ?
           lem12 : suc (c1 n (suc i)) ≤ count-A i  -- becase count-A i contains (ani (suc n))
           lem12 = ?
     ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim (nisa ? )
-    ... | no nisa | tri> ¬a ¬b c₁ = ?
-    ... | yes isa | tri< a ¬b ¬c = ?   -- count-A contains (suc i), so keep ≤-relation
-    ... | yes isa | tri≈ ¬a b ¬c = ?
-    ... | yes isa | tri> ¬a ¬b c₁ = ?
+    ... | no nisa | tri> ¬a ¬b c₁ = subst ( λ k → k ≤ count-A i) (c1+0 {n} {i} nisa) (c1<count-A n i)
+    ... | yes isa | tri< a ¬b ¬c = lem12 where  -- count-A contains (suc i), so keep ≤-relation
+          lem10 : c1 n i ≤ count-A i
+          lem10 = c1<count-A n i
+          lem11 : c1 n (suc i) ≤ count-A (suc i)
+          lem11 = c1<count-A n (suc i)
+          lem12 : suc (c1 n (suc i)) ≤ suc (count-A i) 
+          lem12 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
+          ... | tri< a ¬b ¬c | eq = s≤s (subst (λ k → k ≤ count-A i) eq (c1<count-A n i))
+          ... | tri≈ ¬a b ¬c | eq = begin
+               suc (c1 n (suc i)) ≡⟨ cong suc (sym eq) ⟩
+               suc (suc ( c1 n i)) ≤⟨ ? ⟩
+               suc (suc (count-A i)) ≤⟨ ? ⟩
+               suc (count-A i) ∎ where open ≤-Reasoning
+          ... | tri> ¬a ¬b c₁ | t = ?
+    ... | yes isa | tri≈ ¬a b ¬c = lem12 where  -- count-A contains (suc i), so keep ≤-relation
+          lem10 : c1 n i ≤ count-A i
+          lem10 = c1<count-A n i
+          lem12 : suc (c1 n (suc i)) ≤ suc (count-A i) 
+          lem12 = ?
+    ... | yes isa | tri> ¬a ¬b c₁ = lem12 where -- count-A is one degree larger now
+          open ≤-Reasoning
+          lem10 : c1 n i ≤ count-A i
+          lem10 = c1<count-A n i
+          lem12 : c1 n (suc i) ≤ suc (count-A i) 
+          lem12 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
+          ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<count-A n i)) a≤sa
+          ... | tri≈ ¬a b ¬c | eq = begin
+               c1 n (suc i) ≡⟨ sym eq ⟩
+               suc ( c1 n i) ≤⟨ s≤s (c1<count-A n i) ⟩
+               suc (count-A i) ∎ 
+          ... | tri> ¬a ¬b c₁ | eq = begin
+               c1 n (suc i) ≡⟨ sym eq ⟩
+               suc ( c1 n i) ≤⟨ s≤s (c1<count-A n i) ⟩
+               suc (count-A i) ∎ 
 
     record maxAC (n : ℕ) : Set where
        field