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

diff -r db8229569750 -r e3302db6bbdc src/bijection.agda
--- a/src/bijection.agda	Mon Jun 19 07:11:04 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 08:11:48 2023 +0900
@@ -932,58 +932,56 @@
              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) 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₁ = 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) ∎ 
+    ... | no nisa | tri< a ¬b ¬c = lem12 where
+         lem12 : 1 ≤ count-A i  -- ca contains ani 0
+         lem12 = ?
+    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa ? )
+    ... | no nisa | tri> ¬a ¬b c₁ = z≤n 
+    ... | yes isa | tri< a ¬b ¬c = s≤s z≤n
+    ... | yes isa | tri≈ ¬a b ¬c = s≤s z≤n
+    ... | yes isa | tri> ¬a ¬b c₁ = z≤n
+    c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) 
+    ... | no nisa = ca00 where
+       ca00 : c1 (suc n) (suc i) ≤ count-A i
+       ca00 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
+       ... |  tri< a ¬b ¬c = lem12 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
+             lem12 : suc (c1 n (suc i)) ≤ count-A i  -- becase count-A i contains (ani (suc n))
+             lem12 = ?
+       ... |  tri≈ ¬a b ¬c = ⊥-elim (nisa ? )
+       ... |  tri> ¬a ¬b c₁ = subst ( λ k → k ≤ count-A i) (c1+0 {n} {i} nisa) (c1<count-A n i)
+    ... | yes isa = ca01 where
+       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) ∎ 
+       ca01 : c1 (suc n) (suc i) ≤ suc (count-A i)
+       ca01 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
+       ... | tri< a ¬b ¬c = lem13 where  -- count-A contains (suc i), so keep ≤-relation
+             lem11 : c1 n (suc i) ≤ count-A (suc i)
+             lem11 = c1<count-A n (suc i)
+             lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
+             lem13 = ?
+       ... | tri≈ ¬a b ¬c = ? where  -- count-A contains (suc i) here
+             lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
+             lem13 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 bi ¬c | eq = ?
+             ... | tri> ¬a ¬b c₁ | eq = ?
+       ... | tri> ¬a ¬b c₁ = lem12 -- count-A is one degree larger now
 
     record maxAC (n : ℕ) : Set where
        field