# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686396148 -32400
# Node ID a6e3fa2ded0045f0fb0e47ed0782a7bc24b81500
# Parent  08cd04cc33fec750cf0cc717714b11e650d97253
bad appraoch

diff -r 08cd04cc33fe -r a6e3fa2ded00 src/bijection.agda
--- a/src/bijection.agda	Sat Jun 10 16:22:47 2023 +0900
+++ b/src/bijection.agda	Sat Jun 10 20:22:28 2023 +0900
@@ -589,7 +589,6 @@
        field
            ac : ℕ
            n<ca : n < count-A ac
-           full : ac < count-A n → n ≡ ac 
 
     record maxACN (n : ℕ) : Set where
        field
@@ -612,61 +611,22 @@
             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) ; full = λ _ → refl }
+                ... | 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 ; full = ? }
+                ... | 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) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j)))
-            ... | tri< a ¬b ¬c = record { ac = maxAC.ac (lem10 j) ; n<ca = a ; full = ? } -- 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 ; full = ? } where
-                -- 
-                -- then suc j ≡ count-A (maxAC.ac (lem10 j))
-                --   it means count-A is full
-                --      the new one must be above
-                --
-                lem40 : (j : ℕ) → maxAC.ac (lem10 j) < count-A j → j ≡ maxAC.ac (lem10 j)
-                lem40 j j<ca = maxAC.full (lem10 j) j<ca
-                lem31 :  suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) 
-                lem31 with <∨≤  j (fun→ cn (g (f (fun← an (suc j)))))
-                ... | case1 lt = lem12 _ lt ≤-refl  where
-                     lem13 : j < fun→ cn (g (f (fun← an (suc j))))
-                     lem13 = lt
-                     -- suc j is current count of A
-                     -- it increase at fun→ cn (g (f (fun← an (suc j))))
-                     -- otherwise ≤
-                     lem12 : (i : ℕ) → j < i  → i ≤ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A i
-                     lem12 (suc i) (s≤s sj<i) i≤fj with ≤-∨ sj<i
-                     ... | case1 refl = lem16 where -- subst (λ k → k < count-A (suc i)) (sym eq) lem16 where
-                         lem17 : i < count-A i
-                         lem17 = subst (λ k → i  < k ) ? a<sa
-                         lem16 : suc i < count-A (suc i)
-                         lem16 = ?
-                     ... | case2 lt = ≤-trans lem14 lem15  where
-                         lem14 : suc j < count-A i
-                         lem14 = lem12 i lt (≤-trans refl-≤s i≤fj)
-                         lem15 : count-A i ≤ count-A (suc i)
-                         lem15 = count-A-≤cong refl-≤s 
-                ... | 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
+            lem10 (suc j) = nac where
+                ac = maxAC.ac (lem10 j)
+                nac : maxAC (suc j)
+                nac with <-cmp ac (fun→ cn (g (f (fun← an (suc j)))))
+                ... | tri< a ¬b ¬c = record { ac = fun→ cn (g (f (fun← an (suc j)))) ; n<ca = ? } 
+                ... | tri≈ ¬a b ¬c = record { ac = ac ; n<ca = ? } 
+                ... | tri> ¬a ¬b c = record { ac = ac ; n<ca = ? } 
+                lem14 : j < count-A ac
+                lem14 = ?
+                lem13 : (i : ℕ) → i ≤ nac →  suc j < count-A i
+                lem13 i i≤n = ?
 
     lem01 : (n i : ℕ) → n < count-B i → B
     lem01 zero zero lt with is-B (fun← cn zero)