# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686961860 -32400
# Node ID 7af7fda7d6697ba2496423151fae79ddc1ed0d22
# Parent  884f5fcd41dc54913c414857be7cdd784154fd2f
...

diff -r 884f5fcd41dc -r 7af7fda7d669 src/bijection.agda
--- a/src/bijection.agda	Sat Jun 17 08:20:04 2023 +0900
+++ b/src/bijection.agda	Sat Jun 17 09:31:00 2023 +0900
@@ -670,10 +670,6 @@
     ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
 
-    --
-    -- c n < i means j < suc n → fun← an j < c n, we cannot have more else
-    --    ∃ j → j < suc n → c n < fun← an j
-    --
     c1-max : (n i : ℕ) → c n < i → c1 n i ≡ suc n
     c1-max zero i cn<i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
     ... | tri< a ¬b ¬c = refl
@@ -706,26 +702,22 @@
     ani : (i : ℕ) → ℕ
     ani i = fun→ cn (g (f (fun← an i))) 
 
+    i-in-n : (i n : ℕ) → i ≤ n → Set
+    i-in-n i n i≤n = c1 n (suc (c n)) ≤ i
+
     --- c1 n i
-    c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn i)) → fun→  an (Is.a isa) < suc n → suc (c1 n i) ≡ c1 n (suc i)
-    c1+1 0 i isa a<n with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
-    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ?
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ?
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ?
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ?
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ?
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ?
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ?
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ?
-    c1+1 (suc n) i isa a<n with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
-    ... | s | tri< a ¬b ¬c = ?
-    ... | tri< a ¬b ¬c₁ | tri≈ ¬a b ¬c = ?
-    ... | tri≈ ¬a₁ b₁ ¬c₁ | tri≈ ¬a b ¬c = ?
-    ... | tri> ¬a₁ ¬b c₁ | tri≈ ¬a b ¬c = ?
-    ... | tri< a ¬b₁ ¬c | tri> ¬a ¬b c₁ = ?
-    ... | tri≈ ¬a₁ b ¬c | tri> ¬a ¬b c₁ = ?
-    ... | tri> ¬a₁ ¬b₁ c₂ | tri> ¬a ¬b c₁ = ?
+    c1+1P : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn i)) →  Set
+    c1+1P n i isa with <-cmp n (fun→  an (Is.a isa))
+    ... | tri< n<an ¬b ¬c = c1 n i ≡ c1 n (suc i)
+    ... | tri≈ ¬a n=an ¬c = suc (c1 n i) ≡ c1 n (suc i)
+    ... | tri> ¬a ¬b an<n = suc (c1 n i) ≡ c1 n (suc i)
+
+    c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn i)) 
+        →  c1+1P n i isa 
+    c1+1 n i isa with <-cmp n (fun→  an (Is.a isa))
+    ... | tri< j<an ¬b ¬c = ?
+    ... | tri≈ ¬a j=an ¬c = ?
+    ... | tri> ¬a ¬b an<j = ?
 
     record maxAC (n : ℕ) : Set where
        field