# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686320927 -32400
# Node ID 0d2f3a042fa9d952d9a29ae378424a7f9b1a8a7d
# Parent  29637e5921f5b60587a07aa82cb6b8182ce03b35
...

diff -r 29637e5921f5 -r 0d2f3a042fa9 src/bijection.agda
--- a/src/bijection.agda	Fri Jun 09 18:04:08 2023 +0900
+++ b/src/bijection.agda	Fri Jun 09 23:28:47 2023 +0900
@@ -551,23 +551,35 @@
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
-    lem02 : (n i : ℕ) → i ≡ fun→ cn (g (f (fun← an n))) → n < count-A i
-    lem02 zero zero eq with is-A (fun← cn zero)
-    ... | yes isA = ≤-refl
-    ... | no nisA = ⊥-elim (nisA record { a = (fun← an zero) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
-    lem02 zero (suc i) eq with is-A (fun← cn (suc i))
-    ... | yes isA = s≤s z≤n
-    ... | no nisA = ⊥-elim (nisA record { a = (fun← an zero) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
-    lem02 (suc n) zero eq with is-A (fun← cn zero)
-    ... | yes isA = ?
-    ... | no nisA = ⊥-elim (nisA record { a = (fun← an (suc n)) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
-    lem02 (suc n) (suc i) eq with is-A (fun← cn (suc i))
-    ... | yes isA = ? where
-          --  nth a can be larger than (n+1)th
-          lem04 : n < count-A (fun→ cn (g (f (fun← an n))))
-          lem04 = lem02 n _ refl
-    ... | no nisA = ⊥-elim (nisA record { a = (fun← an (suc n)) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
-    
+    record maxAC (n : ℕ) : Set where
+       field
+           ac : ℕ
+           n<ca : n < count-A ac
+
+    record maxACN (n : ℕ) : Set where
+       field
+           acn : ℕ
+           cn<acn : (i : ℕ) → i ≤ n → fun→ cn (g (f (fun← an i))) ≤ acn
+
+    lem02 : (n : ℕ) → maxAC n
+    lem02 n = lem03 _ n ≤-refl where 
+        maxac : (i : ℕ) → maxACN i
+        maxac zero = record { acn = fun→ cn (g (f (fun← an zero))) ; cn<acn = ? }
+        maxac (suc i) with <-cmp (fun→ cn (g (f (fun← an (suc i))))) (maxACN.acn (maxac i))
+        ... | tri< a ¬b ¬c = record { acn = maxACN.acn (maxac i) ; cn<acn = ? }
+        ... | 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 j : ℕ) → i ≤ maxACN.acn (maxac j) → maxAC j
+        lem03 zero zero z≤n 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) }
+        ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an (maxACN.acn (maxac zero)) ; fa=c = ? } ) where
+             lem04 : InjectiveF.f gi (InjectiveF.f fi (fun← an zero)) ≡ fun← cn 0
+             lem04 with maxACN.cn<acn (maxac zero) 0 ≤-refl
+             ... | t = ?
+        lem03 (suc i) zero i≤m = ?
+        lem03 i (suc j) i≤m = ?
+
+
     lem01 : (n i : ℕ) → n < count-B i → B
     lem01 zero zero lt with is-B (fun← cn zero)
     ... | yes isB = Is.a isB
@@ -577,20 +589,16 @@
     ... | no nisB = lem01 zero i lt 
     lem01 (suc n) zero lt with is-B (fun← cn zero)
     ... | yes isB = Is.a isB
-    ... | no nisB = ? -- ⊥-elim (¬a≤a lt)
+    ... | no nisB = ⊥-elim (nat-≤>  lt 0<s )
     lem01 (suc n) (suc i) lt with is-B (fun← cn (suc i))
     ... | yes isB = Is.a isB
     ... | no nisB = lem01 (suc n) i lt 
 
     ntob : (n : ℕ) → B
-    ntob n = lem01 n (fun→ cn (g (f (fun← an n)))) (≤-trans (lem02 n _ refl ) (ca≤cb0 (fun→ cn (g (f (fun← an n)))))) 
+    ntob n = 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 (lem02 n _ refl ) (ca≤cb0 (fun→ cn (g (f (fun← an n)))))) refl where
-        lem03 :  (i : ℕ) → (lt : n < count-B i )
-           → i ≡ (fun→ cn (g (f (fun← an n))))
-           → count-B (fun→ cn (g (lem01 n i lt ))) ≡ n
-        lem03 = ?
+    biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl 
 
     biso1 : (b : B) → ntob (bton b) ≡ b
     biso1 b = ?