# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686622925 -32400
# Node ID 75894c1665f78869451759feddef57f15d6f6491
# Parent  17a8e67ec12435bc5b949a2a2d579a5c9efed8dc
...

diff -r 17a8e67ec124 -r 75894c1665f7 src/bijection.agda
--- a/src/bijection.agda	Tue Jun 13 08:42:46 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 11:22:05 2023 +0900
@@ -778,59 +778,30 @@
          flen =  Data.List.Fresh.length 
          len=n : flen (FLany.flist fa) ≡ suc n
          len=n = ?
+         fli : FL fm → ℕ
+         fli (ca<n i x) = i
          flist-top : (fl : FList fm) → 0 < flen fl  → ℕ
          flist-top [] ()
          flist-top (cons (ca<n i x₁) fl x) _ = fun→ cn (g (f (fun← an i)))
-         n<ca1 : ( fl : FList fm) → (0<fl : 0 < flen fl ) → flen fl + count-A (flist-top fl 0<fl ) ≤ count-A fm
-         n<ca1 [] _ = ≤-trans ? ( count-A-mono {0} {fm} z≤n )
-         n<ca1 (cons (ca<n i ci≤fm) [] fr) 0<fl = ?
-         n<ca1 (cons (ca<n i ci≤fm) (cons a fl fr0) fr) 0<fl = ? where
-            lem10 : flen fl + count-A (flist-top fl ? ) ≤ count-A fm
-            lem10 = n<ca1 fl ?
-            lem11 : suc (suc ? + count-A (fun→ cn (g (f (fun← an i))))) ≤ count-A fm
-            lem11 = begin
-               ? ≡⟨ ? ⟩ 
-               suc (flen fl + count-A (fun→ cn (g (f (fun← an i))))) ≡⟨ refl ⟩ 
-               (1 + flen fl ) + count-A (fun→ cn (g (f (fun← an i)))) ≡⟨ cong (λ k → k + count-A (fun→ cn (g (f (fun← an i))))) (+-comm 1 _) ⟩ 
-               (flen fl + 1) + count-A (fun→ cn (g (f (fun← an i)))) ≡⟨ ( +-assoc ( flen fl) 1  _ ) ⟩ 
-               flen fl + (suc (count-A (fun→ cn (g (f (fun← an i)))))) ≡⟨ ? ⟩ 
-               flen fl + count-A (suc (fun→ cn (g (f (fun← an i))))) ≤⟨ ≤-plus-0 ( count-A-mono (lem12 fl ? )) ⟩ 
-               flen fl + count-A (flist-top fl ? ) ≤⟨ n<ca1 fl ? ⟩
-               count-A fm ∎ where
-                  open ≤-Reasoning
-                  lem12 : (fl : FList fm) → fresh (FL fm) ⌊ _f<?_ ⌋  _ fl  → suc (fun→ cn (g (f (fun← an i)))) ≤ flist-top fl ?
-                  lem12 (cons (ca<n j x₂) fl1 x1) (lift lt1 , fr2) = begin
-                     suc (fun→ cn (g (f (fun← an i)))) ≤⟨ ttf1 lt1  ⟩
-                     fun→ cn (g (f (fun← an j))) ∎ where 
-                        open ≤-Reasoning 
-                        ttf1 : True (ca<n i ci≤fm f<? ca<n j x₂) 
-                          →  suc (fun→ cn (g (f (fun← an i)))) ≤ fun→ cn (g (f (fun← an j)))
-                        ttf1 t = toWitness t
-                  lem12 [] (lift tt) = ?
+         flist-2nd : (fl : FList fm) → 1 < flen fl  → ℕ
+         flist-2nd [] ()
+         flist-2nd (cons (ca<n i x₁) [] x) (s≤s ()) --  = fun→ cn (g (f (fun← an i)))
+         flist-2nd (cons (ca<n i ai<m) (cons j fl frj) fri) (s≤s 0<fl) = fun→ cn (g (f (fun← an (fli j))))
+         flist-last : (fl : FList fm) → 0 < flen fl  → ℕ
+         flist-last (cons i [] x) 0<fl = fun→ cn (g (f (fun← an (fli i))))
+         flist-last (cons i (cons j fl x) y) 0<fl = flist-last (cons j fl x) cl04 where
+             cl04 : 0 < flen (cons j fl x) 
+             cl04 = ≤-trans (s≤s z≤n) a<sa
+         cl00 : (fl : FL fm) → suc (count-A (fli fl)) ≡ count-A (suc (fli fl))
+         cl00 = ?
+         cl01 : (fl : FList fm) → (1<fl : 1 < flen fl ) → flist-top fl (<-trans a<sa 1<fl) < flist-2nd fl 1<fl
+         cl01 = ?
+         n<ca : (fl : FList fm) → flen fl ≤ count-A (flist-last fl ? )
+         n<ca [] = z≤n
+         n<ca (cons (ca<n i fi<fm) fl fr) = ? where
+             cl02 : flen fl ≤ count-A (flist-last fl ? )
+             cl02 = n<ca fl 
 
-                  
-
-         c : {i : ℕ} → i < suc n → ℕ 
-         c {i} i<n = ?
-         cn<fm : { i : ℕ} → (i<n : i < suc n ) → c i<n < fla-max n
-         cn<fm = ?
-         c-inc :  { i : ℕ} → (i<n : i < suc n ) → suc (count-A (c i<n)) ≡  count-A (suc (c i<n)) 
-         c-inc = ?
-         n<ca : (i : ℕ) →  (i<n : i < suc n ) → i + count-A (suc (c i<n)) ≤ n + count-A (fla-max n)
-         n<ca zero i<n = lem00 where
-            lem00 : 0 + count-A (c i<n) ≤ n + count-A (fla-max n)
-            lem00 = ?
-         n<ca (suc i) i<n  = lem03 where
-            lem01 : i + count-A (c i<n) ≤ n + count-A (fla-max n)
-            lem01 = n<ca i (<-trans a<sa i<n)
-            lem04 : i + count-A (suc (c i<n)) ≤ n + count-A (fla-max n) 
-            lem04 = ?
-            lem03 : suc (i + count-A (c i<n)) ≤ n + count-A (fla-max n) 
-            lem03 = begin
-                suc (i + count-A (c i<n)) ≤⟨ ? ⟩
-                suc (n + count-A (fla-max n)) ≤⟨ ? ⟩
-                n + count-A (fla-max n) ∎ where
-                   open ≤-Reasoning
 
     record CountB (n : ℕ) : Set where
        field
@@ -843,13 +814,14 @@
     lem01 zero zero lt with is-B (fun← cn zero)
     ... | no nisB = ?
     ... | yes isB = ?
+    lem01 zero (suc i) ()
     lem01 (suc n) zero ()
-    lem01 n (suc i) n≤i with is-B (fun← cn (suc i))
-    ... | no nisB = lem01 n i n≤i
-    ... | yes isB with <-cmp (count-B (suc i)) n
-    ... | tri< a ¬b ¬c = lem01 n i ?
+    lem01 (suc n) (suc i) n≤i with is-B (fun← cn (suc i))
+    ... | no nisB = lem01 (suc n) i n≤i
+    ... | yes isB with <-cmp (count-B (suc i)) (suc n)
+    ... | tri< a ¬b ¬c = lem01 (suc n) i ?
     ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = eq }
-    ... | tri> ¬a ¬b c = lem01 n i ?
+    ... | tri> ¬a ¬b c = lem01 (suc n) i ?
 
 
     ntob : (n : ℕ) → B