# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686641093 -32400
# Node ID 069966121911321952f1a98f89f54cb71479543d
# Parent  87df366f85f367b4b4b5413a9ad7d7aaafc952fd
...

diff -r 87df366f85f3 -r 069966121911 src/bijection.agda
--- a/src/bijection.agda	Tue Jun 13 12:28:04 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 16:24:53 2023 +0900
@@ -757,7 +757,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
@@ -769,8 +769,10 @@
     -- it means
     --    n < count-A (fla-max 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 = ? } where
+    lem02 n = record { ac = fla-max n ; n≤ca = n≤ca1 } where
          fa : FLany n
          fa = flany n
          fm = fla-max n
@@ -785,25 +787,39 @@
          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 = ? -- ≤-trans (s≤s z≤n) a<sa
-         n<ca : (fl : FList fm) → (i : ℕ) → i ≤ flen fl → i + count-A (c fl 0 ?) ≤ count-A (c fl i ? )
-         n<ca [] i i<fl = ?
-         n<ca (cons (ca<n j fi<fm) fl fr) zero i<fl = ? 
+             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
-             cl02 : i + count-A (c fl 0 ?) ≤ count-A (c fl i ? )
-             cl02 = n<ca fl i ?
-             cl05 : count-A (c fl 0 ?) ≡  count-A (c (cons (ca<n j fi<fm) fl fr) 0 ? ) 
-             cl05 = ?
-             cl06 : suc (count-A (c fl i ?)) ≤  count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) 
-             cl06 = ?
-             cl03 : (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 ?) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? )
+             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 ?) ≡⟨ ? ⟩
-                 (suc i) + count-A (c fl 0 ?) ≡⟨ ? ⟩
-                 suc (i + count-A (c fl 0 ?)) ≤⟨ ? ⟩
-                 suc (count-A (c fl i ?)) ≤⟨ ? ⟩
-                 count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) ∎ where
+                 (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
 
 
     record CountB (n : ℕ) : Set where
@@ -813,11 +829,9 @@
           b=cn : fun← cn cb ≡ g b
           cb=n : count-B cb ≡ n
 
-    lem01 : (n i : ℕ) → n < count-B i → CountB n
-    lem01 zero zero lt with is-B (fun← cn zero)
-    ... | no nisB = ?
-    ... | yes isB = ?
-    lem01 zero (suc i) ()
+    lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
+    lem01 zero zero lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? }
+    lem01 zero (suc i) lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? }
     lem01 (suc n) zero ()
     lem01 (suc n) (suc i) n≤i with is-B (fun← cn (suc i))
     ... | no nisB = lem01 (suc n) i n≤i
@@ -828,7 +842,7 @@
 
 
     ntob : (n : ℕ) → B
-    ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))
+    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)))) ))
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
     biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl