# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686365263 -32400
# Node ID b8489dcae23654967299492976abc07f035bff2a
# Parent  1ea21618aa610b0907c57bb9d963f5765d6453e7
...

diff -r 1ea21618aa61 -r b8489dcae236 src/bijection.agda
--- a/src/bijection.agda	Sat Jun 10 08:05:56 2023 +0900
+++ b/src/bijection.agda	Sat Jun 10 11:47:43 2023 +0900
@@ -531,6 +531,40 @@
     ... | yes isb = suc (count-A n)
     ... | no nisb = count-A n
 
+    count-A-≤cong : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j
+    count-A-≤cong {i} {j} i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    ... | case2 i<j = lem00 _ _ i<j where
+         lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-≤cong i<j) (lem01 j) where
+             lem01 : (j : ℕ) → count-A j ≤ count-A (suc j) 
+             lem01 zero with is-A (fun← cn (suc zero))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
+             lem01 (suc n) with is-A (fun← cn (suc (suc n)))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
+
+    count-A<i : (i : ℕ) → count-A i ≤ suc i
+    count-A<i zero with is-A (fun← cn  zero) | inspect ( count-A ) zero
+    ... | yes isa | record { eq = eq1 } = ≤-refl
+    ... | no nisa | record { eq = eq1 } = refl-≤s
+    count-A<i (suc i) with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
+    ... | yes isa | record { eq = eq1 } = s≤s ( count-A<i i )
+    ... | no nisa | record { eq = eq1 } = ≤-trans (count-A<i i ) refl-≤s
+
+    full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i) 
+    full-a zero i<ci with is-A (fun← cn  zero) | inspect ( count-A ) zero
+    ... | yes isa | record { eq = eq1 } = isa
+    ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≡< refl i<ci )
+    full-a (suc i) i<ci with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
+    ... | yes isa | record { eq = eq1 } = isa
+    ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans lem36 lem39) a<sa ) where
+          lem36 : suc (suc i) ≤ count-A i
+          lem36 = i<ci
+          lem39 : count-A i ≤ suc i
+          lem39 = count-A<i i
+
     ¬isA∧isB : (y : C ) →  Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥
     ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where
          lem : g (f (Is.a isa)) ≡ y
@@ -570,11 +604,11 @@
         ... | tri≈ ¬a b ¬c = record { acn = maxACN.acn (maxac i) ; cn<acn = ? }
         ... | tri> ¬a ¬b c = record { acn = fun→ cn (g (f (fun← an (suc i)))) ; cn<acn = ? }
         lem03 : (i : ℕ) → maxAC i
-        lem03 i = lem10 i ? where
+        lem03 i = lem10 i where
             lem11 : (i : ℕ) → i ≤ n → fun→ cn (g (f (fun← an i))) ≤ maxACN.acn (maxac n)
             lem11 i i≤n = maxACN.cn<acn (maxac n) i i≤n
-            lem10 : (j : ℕ) → j ≤ maxACN.acn (maxac n) → maxAC j
-            lem10 zero j≤m = lem12 _ refl  where
+            lem10 : (j : ℕ) → maxAC j
+            lem10 zero = lem12 _ refl  where
                 lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an zero))) → maxAC zero
                 lem12 zero i=z with is-A (fun← cn  zero) | inspect ( count-A ) zero
                 ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = subst (λ k → 0 < k) (sym eq1) (s≤s z≤n) }
@@ -582,15 +616,44 @@
                 lem12 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
                 ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s }
                 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) i=z))  } ) 
-            lem10 (suc j) j≤m = ? where
-                lem13 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → maxAC (suc j)
-                lem13 zero i=z with is-A (fun← cn  zero) | inspect ( count-A ) zero
-                ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = ? }
-                ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) ? ))  } ) 
-                lem13 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
-                ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = ? } --  subst (λ k → 0 < k) (sym eq1) 0<s }
-                ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) ? ))  } ) 
-
+            lem10 (suc j) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j)))
+            ... | tri< a ¬b ¬c = record { ac = maxAC.ac (lem10 j) ; n<ca = a } -- if suc j < count-A (maxAC.ac lem14) , we can reuse lem10 j
+            ... | tri> ¬a ¬b (s≤s c) = ⊥-elim ( nat-≤> c (maxAC.n<ca (lem10 j)))
+            ... | tri≈ ¬a sj=ca ¬c = record { ac = fun→ cn (g (f (fun← an (suc j)))) ; n<ca = lem31 } where
+                -- 
+                -- then suc j ≡ count-A (maxAC.ac (lem10 j))
+                --   it means count-A is full
+                --      the new one must be above
+                --
+                lem31 :  suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) 
+                lem31 with <∨≤  (suc j) (fun→ cn (g (f (fun← an (suc j)))))
+                ... | case1 lt = lem12 _ refl  where
+                     lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) 
+                     lem12 zero i=z with is-A (fun← cn  zero) | inspect ( count-A ) zero
+                     ... | yes isa | record { eq = eq1 } = ?
+                     ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) ? ))  } ) 
+                     lem12 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
+                     ... | yes isa | record { eq = eq1 } = ?
+                     ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) ?))  } ) 
+                ... | case2 le = ? where
+                     -- count-A<i : (i : ℕ) → count-A i ≤ suc i
+                     lem33 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) →  ¬ (i ≤ maxAC.ac (lem10 j)) 
+                     lem33 zero i=f i≤m = ?
+                     lem33 (suc i) si=f= i≤m = ?
+                     lem34 : maxAC.ac (lem10 j) ≤ fun→ cn (g (f (fun← an (suc j))))
+                     lem34 = ?
+                     lem32 : suc j ≤ count-A (fun→ cn (g (f (fun← an (suc j))))) 
+                     lem32 with <∨≤  (count-A (fun→ cn (g (f (fun← an (suc j))))) ) (suc j)
+                     ... | case2 le = le
+                     ... | case1 lt = ?
+                lem30 : maxAC.ac (lem10 j) < fun→ cn (g (f (fun← an (suc j))))
+                lem30 = ?
+                lem20 : suc j ≡ count-A (maxAC.ac (lem10 j))
+                lem20 = sj=ca
+                lem14 : maxAC j
+                lem14 = lem10 j 
+                lem17 : j < count-A (maxAC.ac lem14)
+                lem17 = maxAC.n<ca lem14
 
     lem01 : (n i : ℕ) → n < count-B i → B
     lem01 zero zero lt with is-B (fun← cn zero)