# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686527486 -32400
# Node ID b8f02f27d8ebd0f690bf1cb034b0c69776d564c6
# Parent  1fe857e51f4922963c7a414072ee05c06b714c94
...

diff -r 1fe857e51f49 -r b8f02f27d8eb src/bijection.agda
--- a/src/bijection.agda	Sun Jun 11 21:13:55 2023 +0900
+++ b/src/bijection.agda	Mon Jun 12 08:51:26 2023 +0900
@@ -704,12 +704,6 @@
     insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)
 
 
-    record maxAC (n : ℕ) : Set where
-       field
-           ac : ℕ
-           n<ca : n < count-A ac
-           all-a : (i : ℕ) → i ≤ n → fun→ cn (g (f (fun← an i))) ≤ ac
-
     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)
@@ -741,59 +735,56 @@
     flany : (n : ℕ) → FLany n
     flany n = record { flist = fla0 n n a<sa ; flany = λ j j<n → flany0 n a<sa j j<n (x<sy→x≤y j<n) } where
         flany0  : (i : ℕ) → (i<n : i < suc n ) → (j : ℕ) → (j<n : j < suc n) → j ≤ i → Any ( ca<n j (fla-max< j n j<n ) ≡_) (fla0 i n i<n)
-        flany0 zero i<n zero j<n z≤n = ? where
+        flany0 zero i<n zero j<n z≤n = fl1 where
             fl0 = ca<n zero (fla-max< zero n 0<s )
-            fl1 = x∈FLins fl0 [] 
+            fl1 : Any (_≡_ (ca<n zero (fla-max< zero n j<n))) (FLinsert fl0 [])
+            fl1 = subst (λ k → Any (_≡_ (ca<n zero (fla-max< zero n k))) (FLinsert fl0 []) ) (<-irrelevant _ _) (x∈FLins fl0 [] )
         flany0 (suc i) (s≤s i<n) j j<n j≤i with ≤-∨ j≤i
-        ... | case1 refl = ? where
+        ... | case1 refl = fl3 where
             fl0 : FL (fla-max n )
             fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa) )
             fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n)) 
-            fl3 = x∈FLins fl0 fl1 
+            fl3 : Any (_≡_ (ca<n (suc i) (fla-max< (suc i) n j<n))) (FLinsert (ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa)))
+                 (fla0 i n (s≤s (≤-trans refl-≤s i<n))))
+            fl3 = subst (λ k →  Any (_≡_ (ca<n (suc i) (fla-max< (suc i) n k))) (FLinsert (ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa)))
+                 (fla0 i n (s≤s (≤-trans refl-≤s i<n))))) (<-irrelevant _ _) (x∈FLins fl0 fl1 )
         ... | case2 (s≤s j<i) = insAny fl1 (flany0 i (≤-trans refl-≤s (s≤s i<n)) j j<n j<i) where
             fl0 : FL (fla-max n )
             fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa) )
             fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n)) 
             fl3 = x∈FLins fl0 fl1 
 
- 
+    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
+    --         ∃ 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)
+    --    0 < cm  →          1 < cm                                                → n < cm
+    -- it means
+    --    n < count-A (fla-max n) 
+    --
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = lem03 n where 
-        lem03 : (i : ℕ) → maxAC i
-        lem03 i = lem10 i where
-            lem10 : (j : ℕ) → maxAC j
-            lem10 zero = lem12 _ refl  where
-                lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an zero))) → maxAC zero
-                lem12 zero i=z with is-A (fun← cn  zero) | inspect ( count-A ) zero
-                ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = subst (λ k → 0 < k) (sym eq1) (s≤s z≤n) ; all-a = ? }
-                ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) i=z))  } ) 
-                lem12 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
-                ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s ; all-a = ? }
-                ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) i=z))  } ) 
-            lem10 (suc j) = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? }  where
-                
-                fan = fun→ cn (g (f (fun← an (suc j)))) 
-                ac = maxAC.ac (lem10 j)
-                nac : ℕ
-                nac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j))
-
-                n<ca : suc j < count-A nac
-                n<ca = ? where
-                    n<ca0 : j < count-A (maxAC.ac (lem10 j))
-                    n<ca0 = maxAC.n<ca (lem10 j)
-                    n<ca2 : j < count-A nac
-                    n<ca2 = ≤-trans n<ca0 (count-A-homo (y≤max fan ac))
-                    fun< : (i : ℕ) → count-A (fun→ cn (g (f (fun← an i)))) < count-A (suc (fun→ cn (g (f (fun← an i)))))
-                    fun< = ?
-
-                    n<ca1 : (i n : ℕ ) → i ≤ suc j → n ≤ nac  →  i < count-A n
-                    n<ca1 zero n with is-A (fun← cn zero)
-                    ... | yes isa = ?
-                    ... | no nisa = ?
-                    n<ca1 (suc i) n with is-A (fun← cn (suc i))
-                    ... | yes isa = ? -- n<ca1 ?
-                    ... | no nisa = ? -- n<ca1 ?
-
+    lem02 n = record { ac = fla-max n ; n<ca = ? } where
+         fa : FLany n
+         fa = flany n
+         fm = fla-max n
+         cm = count-A fm
+         c : FL fm → ℕ 
+         c fl = ?
+         cn<fm : (fl : FL fm) → c fl < fla-max n
+         cn<fm = ?
+         c-inc : (fl : FL fm) → suc (count-A (c fl)) ≡  count-A (suc (c fl)) 
+         c-inc = ?
+         len=n : (x : FList fm) → Data.List.Fresh.length x ≡ suc n
+         len=n = ?
+         n<ca : (i j : ℕ) → j + i ≡ n → count-A j + i < count-A (fla-max n) 
+         n<ca i j j+i=n = ?
 
     record CountB (n : ℕ) : Set where
        field