--- a/src/bijection.agda	Fri Jun 16 21:39:50 2023 +0900
+++ b/src/bijection.agda	Sat Jun 17 08:20:04 2023 +0900
@@ -606,6 +606,7 @@
     c zero = fun→ cn (g (f (fun← an zero)))
     c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
 
+
     c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
     c< zero zero (s≤s z≤n) = a<sa
     c< (suc i) zero  (s≤s ())
@@ -677,37 +678,54 @@
     c1-max zero i cn<i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
     ... | tri< a ¬b ¬c = refl
     ... | tri≈ ¬a b ¬c = refl
-    ... | tri> ¬a ¬b c₁ = ?
-    c1-max (suc n) i cn<i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
-    ... | tri< a ¬b ¬c = cong suc (c1-max n i ? )
-    ... | tri≈ ¬a b ¬c = cong suc (c1-max n i ? )
-    ... | tri> ¬a ¬b c₁ = ?
+    ... | tri> ¬a ¬b c₁ = ⊥-elim (c100 cn<i)  where
+       c100 : ¬ ( suc (fun→ cn (g ( f ( fun← an 0)))) ≤ i )
+       c100 f<i = nat-≤> (s≤s c₁) (<-transʳ f<i (<-trans a<sa a<sa))
+    c1-max (suc n) i cn<i = c101 where
+        m<i : fun→ cn (g (f (fun← an (suc n))))  < i
+        m<i = begin
+           suc (fun→ cn (g (f (fun← an (suc n)))))  ≤⟨ s≤s (x≤max _ _) ⟩
+           suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n))  ≤⟨ cn<i ⟩
+           i ∎ where 
+             open ≤-Reasoning
+        c102 : c n < i
+        c102 = begin
+           suc (c n)  ≤⟨ s≤s (y≤max _ _) ⟩
+           suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n))  ≤⟨ cn<i ⟩
+           i ∎ where 
+             open ≤-Reasoning
+        c101 : c1 (suc n) i ≡ suc (suc n)
+        c101 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
+        ... | tri< a ¬b ¬c = cong suc (c1-max n i c102 )
+        ... | tri≈ ¬a b ¬c = cong suc (c1-max n i c102 )
+        ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-<> c₁ m<i )
+
+    gf-is-a :  (i : ℕ) → Is A C (λ i → g (f i)) (g (f (fun← an i))) 
+    gf-is-a i = record { a = fun← an i ; fa=c = refl }
+
+    ani : (i : ℕ) → ℕ
+    ani i = fun→ cn (g (f (fun← an i))) 
 
     --- c1 n i
-    c1+1 : (n i : ℕ) → i < c n → Is A C (λ i → g (f i)) (g (f (fun← an i))) → suc (c1 n i) ≡ c1 n (suc i)
-    c1+1 zero i i<c0 isa = c1+10 where
-        c1+10 : suc (c1 zero i) ≡ c1 zero (suc i)
-        c1+10 with <-cmp (fun→ cn (g (f (fun← an zero)))) i
-        ... | tri≈ ¬a b ¬c = ⊥-elim (¬a ? )
-        ... | tri> ¬a ¬b c = ?
-        ... | tri< a ¬b ¬c with is-A (g (f (fun← an zero)))
-        ... | yes _ = ?
-        ... | no _  = ?
-    c1+1 (suc n) i i<cn isa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
-    ... | tri≈ ¬a b ¬c = ? -- c1+1 n i ?
-    ... | tri> ¬a ¬b c = ? -- c1+1 n i ?
-    ... | tri< a ¬b ¬c with is-A (g (f (fun← an (suc n))))
-    ... | yes _ = ? -- cong suc (c1+1 n i ?)
-    ... | no _  = ? --      c1+1 n i ?
-
-    c1=c1 : (n i : ℕ) → i < c n → ¬ (Is A C (λ i → g (f i)) (g (f (fun← an i)))) → c1 n i ≡ c1 n (suc i)
-    c1=c1 = ?
-
-    c1=sn : (n i : ℕ) → c n < i → c1 n i ≡ suc n
-    c1=sn = ?
-
-    c1=count-A : (n i : ℕ) → c n < i → c1 n i ≤ count-A n
-    c1=count-A = ?
+    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₁ = ?
 
     record maxAC (n : ℕ) : Set where
        field