# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686471312 -32400
# Node ID 95f6216499d7c118a5d650f6c22db98543843da3
# Parent  70d46c446b0d379a95f82256027da889840f166d
...

diff -r 70d46c446b0d -r 95f6216499d7 src/bijection.agda
--- a/src/bijection.agda	Sun Jun 11 10:26:09 2023 +0900
+++ b/src/bijection.agda	Sun Jun 11 17:15:12 2023 +0900
@@ -489,7 +489,8 @@
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
 open import Data.Unit.Base using (⊤ ; tt)
 open import Data.List.Fresh hiding ([_])
-
+open import Data.List.Fresh.Relation.Unary.Any 
+open import Data.List.Fresh.Relation.Unary.All 
 
 record InjectiveF (A B : Set) : Set where
    field
@@ -598,8 +599,8 @@
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
-    data  FL : (n : ℕ ) → Set where
-       ca<n : {n : ℕ} → (i : ℕ) →  fun→ cn (g (f (fun← an i))) < n →  FL n
+    data  FL (n : ℕ ) : Set where
+       ca<n : (i : ℕ) →  fun→ cn (g (f (fun← an i))) < n →  FL n
 
     _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  
     _f<_  {n} (ca<n i i<n) (ca<n j j<n) = fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an j))) 
@@ -671,12 +672,55 @@
     FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
         Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y
 
+    x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_) (FLinsert x xs)
+    x∈FLins {zero} f0 [] = here refl
+    x∈FLins {zero} f0 (cons f1 xs x) = here refl
+    x∈FLins {suc n} x [] = here refl
+    x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
+    ... | tri< x<a ¬b ¬c = here refl
+    ... | tri≈ ¬a b ¬c   = here b
+    x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
+    x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
+
     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)
+
+    fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < fla-max n
+    fla-max< zero n i≤n = ?
+    fla-max< (suc i) n i≤n = ?
+
+    record FLany (n m : ℕ ) : Set where
+       field
+          flist  : FList (fla-max n)
+          flany  : (i : ℕ) → (i<n : i < suc m ) → (m≤n : suc m < suc n) → Any ( ca<n i (fla-max< i n (<-trans i<n m≤n )  ) ≡_) flist
+
+    fla : (n : ℕ) → FLany n n
+    fla n = fla0 n a<sa  where
+        fla0 : (i : ℕ ) → i < suc n → FLany n i
+        fla0 zero lt = record { flist = FLinsert fl0 [] ; flany = fl1 } where
+             fl0 : FL (fla-max n )
+             fl0 = ca<n zero (fla-max< zero n 0<s )
+             fl1 : (i : ℕ) (i<n : i < 1) (m≤n : 1 < suc n) → Any (_≡_ (ca<n i (fla-max< i n (<-trans i<n m≤n)))) (FLinsert fl0 [])
+             fl1 zero (s≤s z≤n) lt = x∈FLins fl0 [] 
+        fla0 (suc i) (s≤s lt) = record { flist = FLinsert fl0 fl1 ; flany = fl2 } where
+             fl0 : FL (fla-max n )
+             fl0 = ca<n i (fla-max< i n (≤-trans lt refl-≤s ) )
+             fl1 = FLany.flist ( fla0 i (≤-trans refl-≤s (s≤s lt)) )
+             fl3 = x∈FLins fl0 fl1 
+             fl4 = FLany.flany (fla0 i (≤-trans refl-≤s (s≤s lt))) 
+             fl2 :  (j : ℕ) (i<n : j < suc (suc i)) (m≤n : suc (suc i) < suc n) 
+                  → Any (_≡_ (ca<n j (fla-max< j n (<-trans i<n m≤n)))) (FLinsert fl0 fl1)
+             fl2 j i<n m≤n with ≤-∨ i<n 
+             ... | case1 eq = ?
+             ... | case2 lt = ? -- fl4 ? ? ? -- FLany.flany ( fla0 i ? ) j ? ?
+ 
     lem02 : (n : ℕ) → maxAC n
     lem02 n = lem03 n where 
         lem03 : (i : ℕ) → maxAC i