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

diff -r 0d2f3a042fa9 -r 1ea21618aa61 src/bijection.agda
--- a/src/bijection.agda	Fri Jun 09 23:28:47 2023 +0900
+++ b/src/bijection.agda	Sat Jun 10 08:05:56 2023 +0900
@@ -562,22 +562,34 @@
            cn<acn : (i : ℕ) → i ≤ n → fun→ cn (g (f (fun← an i))) ≤ acn
 
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = lem03 _ n ≤-refl where 
+    lem02 n = lem03 n 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 = ?
+        lem03 : (i : ℕ) → maxAC i
+        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
+                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) }
+                ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) i=z))  } ) 
+                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) ? ))  } ) 
 
 
     lem01 : (n i : ℕ) → n < count-B i → B