# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686713685 -32400
# Node ID d1aae9bbf30c6c82c7fc3f146a032b70cc1b452b
# Parent  93da949d4f83f1e4ca1e5111a2f0e8a874b36256
...

diff -r 93da949d4f83 -r d1aae9bbf30c src/bijection.agda
--- a/src/bijection.agda	Wed Jun 14 09:38:43 2023 +0900
+++ b/src/bijection.agda	Wed Jun 14 12:34:45 2023 +0900
@@ -599,37 +599,53 @@
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
+    --  (c m)  is the number of a of C , where there is (a m)
+    --      c = (g (f (fun← an (a m)))) : C  contains all a which number is less than m 
+    c : (n : ℕ) → ℕ 
+    c zero = fun→ cn (g (f (fun← an zero)))
+    c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
 
-    fla-max : (n : ℕ) → ℕ 
-    fla-max zero = fun→ cn (g (f (fun← an zero)))
-    fla-max (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (fla-max n)
+    a : (n : ℕ) → ℕ 
+    a zero = zero
+    a (suc n) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (c n)
+    ... | tri< lt ¬b ¬c = c n
+    ... | tri≈ ¬a eq ¬c = suc n
+    ... | tri> ¬a ¬b lt = suc n
 
-    fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (fla-max n)
-    fla-max< zero zero (s≤s z≤n) = a<sa 
-    fla-max< (suc i) zero  (s≤s ())
-    fla-max< zero (suc n) (s≤s z≤n) = ≤-trans (fla-max< zero n (<-transʳ  z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (fla-max n)))
-    fla-max< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n
-    ... | case1 refl = s≤s (x≤max  (fun→ cn (g (f (fun← an (suc n))))) (fla-max n))
-    ... | case2 (s≤s (s≤s i<n)) = ≤-trans (fla-max< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (fla-max n)))
+    a=cn : (n : ℕ) → c n ≡ fun→ cn (g (f (fun← an (a n))))
+    a=cn zero = refl
+    a=cn (suc n) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (c n)
+    ... | tri< lt ¬b ¬c = ?
+    ... | tri≈ ¬a eq ¬c = ?
+    ... | tri> ¬a ¬b lt = ?
+
+    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 ())
+    c< zero (suc n) (s≤s z≤n) = ≤-trans (c< zero n (<-transʳ  z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)))
+    c< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n
+    ... | case1 refl = s≤s (x≤max  (fun→ cn (g (f (fun← an (suc n))))) (c n))
+    ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n)))
 
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
            n<ca : n < count-A ac
+
     --
-    -- we have n C sequcence having n A which is less than fla-max n as FList (fla-max n) , so we have n
-    --    c i =  i th FL (fla-max n) where
+    -- we have n C sequcence having n A which is less than c n as FList (c n) , so we have n
+    --    c i =  i th FL (c n) where
     --         ∃ j → i ≡ fun→ cn (g (f (fun← an j)))   by FList n
-    --    cm =     count-A (fla-max n)
-    --    0 < suc (count-A (c 0)) ≡  count-A (suc (c 0)) ≤ count-A (c 1) < ... < suc (count-A (c n)) ≤ count-A (fla-max n)
+    --    cm =     count-A (c n)
+    --    0 < suc (count-A (c 0)) ≡  count-A (suc (c 0)) ≤ count-A (c 1) < ... < suc (count-A (c n)) ≤ count-A (c n)
     --    0 < cm  →          1 < cm                                                → n < cm
     -- it means
-    --    n < count-A (fla-max n) 
+    --    n < count-A (c n) 
     --
     cl07 : { i j : ℕ } → suc i < suc j → i < j
     cl07 {i} {j} (s≤s lt) = lt
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = record { ac = fla-max n ; n<ca = n<ca n } where
+    lem02 n = record { ac = c n ; n<ca = n<ca n } where
          ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i)))) 
          ca+1 i i<ca with fun→ cn (g (f (fun← an i))) | inspect (fun→ cn) (g (f (fun← an i))) 
          ... | suc ca | record { eq = eq1 } with is-A (fun← cn (suc ca))
@@ -642,20 +658,28 @@
                 g (f ( fun← an i)) ≡⟨ sym (fiso← cn _)  ⟩
                 fun← cn (fun→ cn (g (f ( fun← an i)))) ≡⟨ cong (fun← cn) eq1 ⟩
                 fun← cn (suc ca) ∎ where open ≡-Reasoning
-         n<ca : (n : ℕ ) → n < count-A (fla-max n) 
-         n<ca zero with is-A (g (f (fun← an zero)))
-         ... | yes isa = ?
-         ... | no nisa = ?
-         n<ca (suc n) with is-A (g (f (fun← an (suc n))))
-         ... | no nisa = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = refl } ) 
-         ... | yes isa = ?
-         -- cl25 where
-         --     cl00 : n < count-A (fla-max n)
-         --     cl00 = n<ca n
-         --     cl01 : count-A (suc n) < count-A (fun→ cn (g (f (fun← an (suc n))))) 
-         --     cl01 = ca+1 (suc n) ?
-         --     cl25 : suc n < count-A (max (fun→ cn (g (f (fun← an (suc n))))) (fla-max n))
-         --     cl25 = ?
+         n<ca : (n : ℕ ) → n < count-A (c n) 
+         n<ca zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero))) 
+         ... | zero | record { eq = eq1 } = cl23 where
+             cl23 : 1 ≤ count-A zero
+             cl23 = ?
+         ... | suc ca | record { eq = eq1 } = cl24 where
+             cl24 : 1 ≤ count-A (suc ca)
+             cl24 = ?
+         n<ca (suc n) with fun→ cn (g (f (fun← an n))) | inspect (fun→ cn) (g (f (fun← an n))) 
+         ... | zero | record { eq = eq1 } = cl25 where
+             cl25 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n))
+             cl25 = ?
+             --
+             --  count-A (c m)                                                           < count (c (suc m))           ≤ count (c n)
+             --  fun→ cn (g (f (fun← an i)))  <  suc (fun→ cn (g (f (fun← an (suc n))))) ≤ fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n
+             --       c i                                                                 c       (suc i)             c n
+             --  fun→ cn (g (f (fun← an i)))  <  fun→ cn (g (f (fun← an (suc n))))       < fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n
+             --       c i                             c (suc i)                             c (suc (suc i))             c (suc n)
+             --  count-A (c m) = count-A (c (suc m))  count-A (c (suc m))                  < count (c (suc (suc m))       ≤ count (c (suc n))
+         ... | suc ca | record { eq = eq1 } = ? where
+             cl26 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n))
+             cl26 = ?
          -- = <-transʳ (count-A-mono ?) (ca+1 zero ?) where
 
     record CountB (n : ℕ) : Set where