# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686414046 -32400
# Node ID 1f43bbfff797fa8b55558bdaecf17ba6092c14a7
# Parent  46d2c0341fcbd36c64818275a0ec4605bb4bc37a
...

diff -r 46d2c0341fcb -r 1f43bbfff797 src/bijection.agda
--- a/src/bijection.agda	Sat Jun 10 22:42:45 2023 +0900
+++ b/src/bijection.agda	Sun Jun 11 01:20:46 2023 +0900
@@ -531,12 +531,12 @@
     ... | 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
+    count-A-homo : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j
+    count-A-homo {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
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-homo 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
@@ -604,14 +604,27 @@
                 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 ; all-a = ? }
                 ... | 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) = record { ac = nac ; n<ca = ? ; all-a = ? } where
+            lem10 (suc j) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j)))
+            ... | tri< a ¬b ¬c = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? } 
+            ... | tri> ¬a ¬b ca<sj = ? --   maxAC (suc j) contains at least (suc j) elements of A
+            ... | tri≈ ¬a sj=ca ¬c = record { ac = nac ; n<ca = ? ; all-a = ? } where
                 -- 
-                --   maxAC n contains at least n elements of A
-                --
+                -- maxAC contains all 0 to j th element of A and nothing else
+                --    using full-a, we can take fun← cn which is smaller than suc j
+                --    so it cannot be fan.
+                
+                fan = fun→ cn (g (f (fun← an (suc j)))) 
+                ac = maxAC.ac (lem10 j)
                 nac : ℕ
                 nac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j))
+
                 n<ca : suc j < count-A nac
                 n<ca = ? where
+                    n<ca0 : j < count-A (maxAC.ac (lem10 j))
+                    n<ca0 = maxAC.n<ca (lem10 j)
+                    n<ca2 : j < count-A nac
+                    n<ca2 = ≤-trans n<ca0 (count-A-homo (y≤max fan ac))
+
                     n<ca1 : (i n : ℕ ) → i ≤ suc j → n ≤ nac  →  i < count-A n
                     n<ca1 zero n with is-A (fun← cn zero)
                     ... | yes isa = ?
@@ -621,21 +634,6 @@
                     ... | no nisa = ? -- n<ca1 ?
 
 
-    lem01 : (n i : ℕ) → n < count-B i → B
-    lem01 zero zero lt with is-B (fun← cn zero)
-    ... | yes isB = Is.a isB
-    ... | no nisB = ⊥-elim (¬a≤a lt)
-    lem01 zero (suc i) lt with is-B (fun← cn (suc i))
-    ... | yes isB = Is.a isB
-    ... | no nisB = lem01 zero i lt 
-    lem01 (suc n) zero lt = ? -- cannot happen
-    lem01 (suc n) (suc i) lt with is-B (fun← cn (suc i))
-    ... | no nisB = lem01 (suc n) i lt 
-    ... | yes isB with <-cmp n i
-    ... | tri< a ¬b ¬c = lem01 n i ?
-    ... | tri≈ ¬a b ¬c = Is.a isB
-    ... | tri> ¬a ¬b c = ? -- cannot happen
-
     record CountB (n : ℕ) : Set where
        field
           b : B
@@ -643,21 +641,21 @@
           b=cn : fun← cn cb ≡ g b
           cb=n : count-B cb ≡ n
 
-    lem011 : (n i : ℕ) → n ≤ count-B i → CountB n
-    lem011 zero zero z≤n with is-B (fun← cn zero)
+    lem01 : (n i : ℕ) → n < count-B i → CountB n
+    lem01 zero zero lt with is-B (fun← cn zero)
     ... | no nisB = ?
     ... | yes isB = ?
-    lem011 (suc n) zero ()
-    lem011 n (suc i) n≤i with is-B (fun← cn (suc i))
-    ... | no nisB = lem011 n i n≤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 = lem011 n i ?
+    ... | tri< a ¬b ¬c = lem01 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 = lem011 n i ?
+    ... | tri> ¬a ¬b c = lem01 n i ?
 
 
     ntob : (n : ℕ) → B
-    ntob n = 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 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 
diff -r 46d2c0341fcb -r 1f43bbfff797 src/nat.agda
--- a/src/nat.agda	Sat Jun 10 22:42:45 2023 +0900
+++ b/src/nat.agda	Sun Jun 11 01:20:46 2023 +0900
@@ -59,6 +59,18 @@
 max (suc x) zero = (suc x)
 max (suc x) (suc y) = suc ( max x y )
 
+x≤max : (x y : ℕ) → x ≤ max x y
+x≤max zero zero = ≤-refl
+x≤max zero (suc x) = z≤n
+x≤max (suc x) zero = ≤-refl
+x≤max (suc x) (suc y) = s≤s( x≤max x y )
+
+y≤max : (x y : ℕ) → y ≤ max x y
+y≤max zero zero = ≤-refl
+y≤max zero (suc x) = ≤-refl
+y≤max (suc x) zero = z≤n
+y≤max (suc x) (suc y) = s≤s( y≤max x y )
+
 -- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )