# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687311216 -32400
# Node ID 07fe8f8bb6d336d03f4b6c6ecb15cdddcac705af
# Parent  4e1150abfb86a18921a1209bb596fd2b7edc4fd7
...

diff -r 4e1150abfb86 -r 07fe8f8bb6d3 src/bijection.agda
--- a/src/bijection.agda	Tue Jun 20 19:24:48 2023 +0900
+++ b/src/bijection.agda	Wed Jun 21 10:33:36 2023 +0900
@@ -702,10 +702,14 @@
         ... | yes _ = cong suc (lem02 n t refl)
         ... | no _ = lem02 n t refl
 
+    --  remove (ani i) from clist (c n)
+    --
     a-list : (i : ℕ) → (cl : List C) → Any (_≡_ (g (f (fun← an i)))) cl → List C
     a-list i (_ ∷ t) (here px) = t
     a-list i (h ∷ t) (there a) = h ∷ ( a-list i t a )
 
+    --  count of a in a-list is one step reduced
+    --
     a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
         → suc (ca-list (a-list i cl a)) ≡ ca-list cl
     a-list-ca i cl a = lem03 i cl _ a refl where
@@ -720,14 +724,62 @@
          ... | yes y = refl
          ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } )
 
+    --  reduced list still have all ani j < i
+    --
+    a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
+         → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) 
+    a-list-any i cl a j j<i b = lem03 i cl _ a refl j j<i b where
+         lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )  
+             → cal ≡  (a-list i cl a) 
+             → (j : ℕ) → j < i  → Any (_≡_ (g (f (fun← an j)))) cl  → Any (_≡_ (g (f (fun← an j)))) cal
+         lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< 
+             (  bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) j<i )
+         lem03 i (h ∷ t) cal (here px) eq j j<i (there b) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b
+         lem03 i (h ∷ t) cal (there a) eq j j<i (here px) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) (here px)
+         lem03 i (h ∷ t) (h1 ∷ cal) (there a) refl j j<i (there b) = there (lem03 i t cal a refl j j<i b)
+
+    any-cl : (i : ℕ) → (cl : List C) → Set
+    any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl
+
+    n<ca-list0 : (n : ℕ) → n < ca-list (clist (c n))
+    n<ca-list0 zero = subst ( λ k → zero < k ) (a-list-ca zero (clist (c zero)) (clist-any zero zero ≤-refl)) ( <-transˡ a<sa (s≤s z≤n )) 
+    n<ca-list0 (suc n) = lem06 where
+         --
+         --  we have ANY i on i ≤ n, so we can remove n element from clist (c n)
+         --  induction on n is no good, because (ani (suc n)) may happen in clist (c n)
+         --  so we cannot recurse on n<ca-list itself.
+         --
+         lem04 : (i : ℕ) → suc i ≤ n → (cl : List C) → suc i < ca-list cl → (ai : Any (_≡_ (g (f (fun← an i)))) cl)  → i < ca-list (a-list i cl ai)
+         lem04 0 0≤n cl i<c ai = sx≤py→x≤y ( begin
+             2 ≤⟨ i<c ⟩
+             ca-list cl  ≡⟨ sym (a-list-ca 0 cl ai) ⟩
+             suc (ca-list (a-list 0 cl ai)) ∎ ) where
+                 open ≤-Reasoning
+         lem04 (suc i) i≤n cl i<c ai = sx≤py→x≤y ( begin
+             suc (suc (suc i)) ≤⟨ ? ⟩ 
+             suc (ca-list (a-list (suc i) cl ai)) ∎ ) where 
+                 open ≤-Reasoning
+         del : (i : ℕ) → i ≤ n → (cl : List C) → any-cl (suc i) cl → List C
+         del = ?
+         del-any : (i : ℕ) → i ≤ n → (cl : List C) → any-cl (suc i) cl  → any-cl i cl  
+         del-any = ?
+         del-ca : (i : ℕ) → (si≤n : i ≤ n ) → (cl : List C) → (a : any-cl (suc i) cl  )
+              → suc (ca-list cl) ≡ ca-list (del i si≤n cl a)
+         del-ca = ?
+         lem06 : suc n < ca-list (clist (c (suc n)))
+         lem06 = lem07 _ (clist (c (suc n))) ≤-refl lem09 where
+            lem07 : (i : ℕ) → (cl : List C) → (si≤n : i ≤ n) → (a : any-cl (suc i) cl) → suc i < ca-list (del i si≤n cl a)
+            lem07 0 cl le a = ?
+            lem07 (suc i) cl le a = <-trans (s≤s lem08) (subst (λ k → k < ca-list (del (suc i) le cl a) ) 
+             (sym (del-ca (suc i) le cl a)) a<sa) where
+                lem08 : suc i < ca-list (del (suc i) le cl a)
+                lem08 = lem07 i (del (suc i) le cl a) (≤-trans a≤sa le) (del-any (suc i) le cl a) 
+            lem10 : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n))
+            lem10 n i le = clist-any n i le
+            lem09 : any-cl (suc n) (clist (c (suc n)))
+            lem09 i le = clist-any (suc n) i le
     n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
-    n<ca-list zero = subst ( λ k → zero < k ) (a-list-ca zero (clist (c zero)) (clist-any zero zero ≤-refl)) ( <-transˡ a<sa (s≤s z≤n )) 
-    n<ca-list (suc n) = begin
-         suc (suc n) ≤⟨ (s≤s (n<ca-list n)) ⟩ 
-         suc (ca-list (clist (c n))) ≡⟨ ? ⟩ 
-         suc (ca-list (a-list (suc n) (clist (c (suc n))) (clist-any (suc n) (suc n) ≤-refl)))
-             ≡⟨ a-list-ca (suc n) (clist (c (suc n))) (clist-any (suc n) (suc n) ≤-refl) ⟩ 
-         ca-list (clist (c (suc n))) ∎ where open ≤-Reasoning
+    n<ca-list n = ? 
 
     n<ca0 : {n : ℕ} → n < count-A (c n)
     n<ca0 = ?