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

diff -r f506b71b08f9 -r 93da949d4f83 src/bijection.agda
--- a/src/bijection.agda	Wed Jun 14 09:02:37 2023 +0900
+++ b/src/bijection.agda	Wed Jun 14 09:38:43 2023 +0900
@@ -599,110 +599,6 @@
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
-    data  FL (n : ℕ ) : Set where
-       ca<n : (i : ℕ) →  fun→ cn (g (f (fun← an i))) < suc 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))) 
-
-    infixr 250 _f<?_
-
-    f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
-    f<-trans {n} {ca<n i x} {ca<n i₁ x₁} {ca<n i₂ x₂} x<y y<z = <-trans x<y y<z
-
-    FL-eq0 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < suc n } {y : fun→ cn (g (f (fun← an j))) < suc n}  
-         → ca<n i x ≡ ca<n j y 
-         → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j)))
-    FL-eq0 {n} {i} {.i} {x} {.x} refl = refl
-
-    -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
-
-    FL-eq1 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < suc n } {y : fun→ cn (g (f (fun← an j))) < suc n}  
-         → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j)))
-         → ca<n i x ≡ ca<n j y 
-    FL-eq1 {n} {i} {j} {x} {y} eq = lem00 i=j where
-        i=j : i ≡ j
-        i=j = bi-inject← an (InjectiveF.inject fi ( InjectiveF.inject gi (bi-inject→ cn eq) ))
-        lem00 : {x : fun→ cn (g (f (fun← an i))) < suc n } {y : fun→ cn (g (f (fun← an j))) < suc n} → i ≡ j → ca<n i x ≡ ca<n j y
-        lem00 {x} {y} refl with <-irrelevant x y
-        ... | refl = refl
-
-    FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
-    FLcmp {n} (ca<n i x) (ca<n j y) with <-cmp (fun→ cn (g (f (fun← an i)))) (fun→ cn (g (f (fun← an j))) )
-    ... | tri< a ¬b ¬c = tri< a (λ eq → ¬b (FL-eq0 eq) ) ¬c 
-    ... | tri≈ ¬a eq ¬c = tri≈ ¬a (FL-eq1 eq) ¬c 
-    ... | tri> ¬a ¬b c = tri> ¬a (λ eq → ¬b (FL-eq0 eq) )  c 
-
-    _f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
-    _f<?_ {n} x y with FLcmp x y
-    ... | tri< a ¬b ¬c = yes a
-    ... | tri≈ ¬a b ¬c = no ¬a
-    ... | tri> ¬a ¬b c = no ¬a
-
-    FList : (n : ℕ ) → Set
-    FList n = List# (FL n) ⌊ _f<?_ ⌋
-
-    ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) →  fresh (FL (n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (n)) ⌊ _f<?_ ⌋  x y
-    ttf _ [] fr = Level.lift tt
-    ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where 
-           ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
-           ttf1 t x<a = f<-trans x<a (toWitness t)
-
-    FLinsert : {n : ℕ } → FL n → FList n  → FList n 
-    FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
-         → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
-    FLinsert {zero} f0 y = f0 ∷# []
-    FLinsert {suc n} x [] = x ∷# []
-    FLinsert {suc n} x (cons a y x₁) with FLcmp x a
-    ... | tri≈ ¬a b ¬c  = cons a y x₁
-    ... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
-    FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
-    FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
-
-    FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
-    FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
-    ... | tri< x<b ¬b ¬c  = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
-    ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
-    ... | tri> ¬a ¬b b<x =  Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
-    FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
-    ... | tri< x<b ¬b ¬c =  Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
-    ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
-    FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
-        Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
-    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₂) )
-
-    FL0uniq : {a b : FL zero} → a ≡ b
-    FL0uniq {ca<n i x} {ca<n j y} = FL-eq1 (trans lem01 (sym lem02))  where
-       lem01 : fun→ cn (g (f (fun← an i))) ≡ 0
-       lem01 with <-cmp (fun→ cn (g (f (fun← an i))))  0
-       ... | tri≈ ¬a b ¬c = b
-       ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c x )
-       lem02 : fun→ cn (g (f (fun← an j))) ≡ 0
-       lem02 with <-cmp (fun→ cn (g (f (fun← an j))))  0
-       ... | tri≈ ¬a b ¬c = b
-       ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c y )
-
-    insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
-    insAny {zero} {f1} {f2} (cons a L xr) (here eq) = here FL0uniq
-    insAny {zero} {f1} {f2} (cons a L xr) (there any) = insAny {zero} {f1} {f2} L any 
-    insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a 
-    ... | tri< x<a ¬b ¬c = there any
-    ... | tri≈ ¬a b ¬c = any
-    insAny {suc n} {a} {h} (cons a [] (Level.lift tt)) (here refl) | tri> ¬a ¬b c = here refl
-    insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl
-    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)
-
 
     fla-max : (n : ℕ) → ℕ 
     fla-max zero = fun→ cn (g (f (fun← an zero)))
@@ -711,55 +607,15 @@
     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) = ?
+    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)))
 
-
-    fla0 : (i n : ℕ ) → i < suc n → FList (fla-max n)
-    fla0 zero n lt = FLinsert fl0 []  where
-        fl0 : FL (fla-max n )
-        fl0 = ca<n zero (fla-max< zero n 0<s )
-    fla0 (suc i) n (s≤s lt) = FLinsert fl0 fl1  where
-        fl0 : FL (fla-max n )
-        fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ lt a<sa) )
-        fl1 = fla0 i n (≤-trans refl-≤s (s≤s lt)) 
-    fla : (n : ℕ) → FList (fla-max n)
-    fla n = fla0 n n a<sa  
-
-    record FLany (n : ℕ ) : Set where
-       field
-          flist  : FList (fla-max n)
-          flany  : (i : ℕ) → (i<n : i < suc n ) →  Any ( ca<n i (fla-max< i n i<n ) ≡_) flist
-
-    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 = fl1 where
-            fl0 = ca<n zero (fla-max< zero n 0<s )
-            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 = 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 : 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
@@ -773,7 +629,7 @@
     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 = ? } where
+    lem02 n = record { ac = fla-max 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))
@@ -786,13 +642,20 @@
                 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
-         ca=n : (n : ℕ ) → n < count-A (fla-max n) 
-         ca=n zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero))) 
-         ... | zero | record { eq = eq1 } = ?
-         ... | suc ca | record { eq = eq1 } = ?
-         ca=n (suc n) with fun→ cn (g (f (fun← an n))) | inspect (fun→ cn) (g (f (fun← an n))) 
-         ... | zero | record { eq = eq1 } = ?
-         ... | suc ca | record { eq = eq1 } = ?
+         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 = ?
          -- = <-transʳ (count-A-mono ?) (ca+1 zero ?) where
 
     record CountB (n : ℕ) : Set where