# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686700957 -32400
# Node ID f506b71b08f91343fe90acaf8f6082decf2c0280
# Parent  069966121911321952f1a98f89f54cb71479543d
direct count A

diff -r 069966121911 -r f506b71b08f9 src/bijection.agda
--- a/src/bijection.agda	Tue Jun 13 16:24:53 2023 +0900
+++ b/src/bijection.agda	Wed Jun 14 09:02:37 2023 +0900
@@ -711,7 +711,8 @@
     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< i (suc n) i≤n with ≤-∨ i≤n
+    fla-max< zero (suc n) (s≤s z≤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)))
 
@@ -757,7 +758,7 @@
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
-           n≤ca : n ≤ count-A 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
@@ -772,55 +773,27 @@
     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≤ca1 } where
-         fa : FLany n
-         fa = flany n
-         fm = fla-max n
-         cm = count-A fm
-         flen =  Data.List.Fresh.length 
-         len=n : flen (FLany.flist fa) ≡ suc n
-         len=n = ?
-         fli : {n : ℕ } → FL n → ℕ
-         fli (ca<n i x) = i
-         c : {n : ℕ} → (fl : FList n) → (i : ℕ) → i < flen fl  → ℕ
-         c (cons i [] x) j <fl = fli i
-         c (cons i (cons j fl x) y) zero 0<fl = fun→ cn (g (f (fun← an (fli j))))
-         c (cons i (cons j fl x) y) (suc k) 0<fl = c (cons j fl x) k cl04 where
-             cl04 : k < flen (cons j fl x) 
-             cl04 = cl07 0<fl
-         n<ca : (fl : FList fm) → (i : ℕ) → (i<fl : i < flen fl ) → i + count-A (c fl 0 (<-transʳ z≤n i<fl)) ≤ count-A (c fl i i<fl )
-         n<ca [] i ()
-         n<ca (cons (ca<n j fi<fm) fl fr) zero i<fl = subst (λ k → 
-               count-A (c (cons (ca<n j fi<fm) fl fr) 0 k) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) zero i<fl))  (<-irrelevant _ _) ≤-refl 
-         n<ca (cons (ca<n j fi<fm) fl fr) (suc i) i<fl = cl03 where
-             i<fli : i < flen fl
-             i<fli = cl07 i<fl
-             i<fl0 : 0 < flen fl
-             i<fl0 = <-transʳ z≤n (cl07 i<fl)
-             cl02 : i + count-A (c fl 0 i<fl0) ≤ count-A (c fl i i<fli )
-             cl02 = n<ca fl i i<fli
-             cl03 : (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 (<-transʳ z≤n i<fl)) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) i<fl )
-             cl03 = begin
-                 (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 (<-transʳ z≤n i<fl)) ≡⟨ cong (λ k → suc (i + count-A k))  cl05  ⟩
-                 (suc i) + count-A (c fl 0 i<fl0 ) ≡⟨ ? ⟩
-                 suc (i + count-A (c fl 0 i<fl0 )) ≤⟨ s≤s cl02 ⟩
-                 suc (count-A (c fl i i<fli)) ≤⟨ cl06 ⟩
-                 count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) i<fl) ∎ where
-                    open ≤-Reasoning
-                    cl05 : c (cons (ca<n j fi<fm) fl fr) 0 (<-transʳ z≤n i<fl) ≡ c fl 0 i<fl0
-                    cl05 = ?
-                    cl06 :  suc (count-A (c fl i i<fli)) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) i<fl ) 
-                    cl06 = ?
-         n<ff : n < flen (fla n)
-         n<ff = ?
-         n≤ca1 : n ≤ count-A (fla-max n)
-         n≤ca1 = begin
-             n ≤⟨ m≤m+n _ _ ⟩
-             n + count-A (c (fla n) 0 (<-transʳ z≤n n<ff)) ≤⟨ n<ca (fla n) n n<ff ⟩
-             count-A (c (fla n) n n<ff) ≤⟨ count-A-mono {c (fla n) n ?} {fla-max n} ? ⟩
-             count-A (fla-max n) ∎ where
-                open ≤-Reasoning
-
+    lem02 n = record { ac = fla-max n ; n<ca = ? } 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))
+         ... | yes isa = <-transʳ ( count-A-mono (px≤py i<ca)) cl22 where
+             cl22 :  count-A (pred (suc ca)) < suc (count-A ca)
+             cl22 = ≤-refl
+         ... | no nisa = ⊥-elim ( nisa record { a = fun← an i ; fa=c = cl21 } ) where
+             cl21 : g (f ( fun← an i)) ≡ fun← cn (suc ca)
+             cl21 = begin
+                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 } = ?
+         -- = <-transʳ (count-A-mono ?) (ca+1 zero ?) where
 
     record CountB (n : ℕ) : Set where
        field
@@ -842,7 +815,7 @@
 
 
     ntob : (n : ℕ) → B
-    ntob n = CountB.b (lem01 n (maxAC.ac (lem02 (suc n))) (≤-trans (maxAC.n≤ca (lem02 (suc n))) (ca≤cb0 (maxAC.ac (lem02 (suc n)))) ))
+    ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
     biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl