--- a/src/bijection.agda	Fri Jun 23 13:20:00 2023 +0900
+++ b/src/bijection.agda	Fri Jun 23 15:36:09 2023 +0900
@@ -614,10 +614,6 @@
         ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))
         ... | case2 (s≤s le) = there (lem00 j le)
 
-    -- cNL : (n : ℕ ) → NL n
-    -- cNL n = record { nlist = clist (c n) ; anyn = λ i le → clist-any n i le } 
-
-
     ca-list : List C → ℕ
     ca-list [] = 0
     ca-list (h ∷ t) with is-A h
@@ -712,6 +708,24 @@
             ca-list cl ∎ where
                 open ≤-Reasoning
 
+    anygb : (b : B) → Any (_≡_ (g b)) (clist (c (fun→ cn (g b))))
+    anygb = ?
+
+    bton1 : B → ℕ
+    bton1 b = bton10 b (clist (c (fun→ cn (g b)))) ? where
+        bton10 : (b : B) → (x : List C) →  Any (_≡_ (g b)) x → ℕ
+        bton10 b (h ∷ t) (here px)  = count-B ( fun→ cn h )
+        bton10 b (h ∷ t) (there ax) = bton10 b t ax
+
+    anycb : (n : ℕ) → Any (λ c₁ → Is B C g c₁ ∧ (count-B (fun→ cn c₁) ≡ n)) (clist (c n))
+    anycb = ?
+
+    ntob1 : (n : ℕ) → B
+    ntob1 n = bton10 n (clist (c n)) ? where
+        bton10 : (n : ℕ) → (x : List C) → Any (λ c → Is B C g c ∧ (count-B (fun→ cn c) ≡ n)) x →  B
+        bton10 n (h ∷ t) (here px) = Is.a (proj1 px)
+        bton10 n (h ∷ t) (there ax) = bton10 n t ax
+
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
@@ -738,14 +752,20 @@
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 
                 ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
             lem12 : (cb1 : ℕ) → 1 ≡ count-B cb1 → 0 ≡ cb1
-            lem12 = ?
+            lem12 cb1 cbeq with <-cmp 0 cb1
+            ... | tri≈ ¬a b ¬c = b
+            ... | tri< a ¬b ¬c = ?
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
         lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
                  ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
             lem12 : (cb1 : ℕ) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
-            lem12 cb cbeq with CountB.cb-inject ( lem09 n (count-B n) ? refl  )
-            ... | t = ?
+            lem12 cb1 cbeq with <-cmp (suc i) cb1
+            ... | tri< a ¬b ¬c = ?
+            ... | tri≈ ¬a b ¬c = b
+            ... | tri> ¬a ¬b c₁ = ?
+            -- with CountB.cb-inject ( lem09 n (count-B n) ? refl  )
+            -- ... | t = ?
         ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
         lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)