# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687477928 -32400
# Node ID ddb581d5599b5d6a6177866e43e1efac94338c61
# Parent  aca9b1e6750388d865b56cebd51f187b1ecb4935
suc n

diff -r aca9b1e67503 -r ddb581d5599b src/bijection.agda
--- a/src/bijection.agda	Fri Jun 23 08:13:22 2023 +0900
+++ b/src/bijection.agda	Fri Jun 23 08:52:08 2023 +0900
@@ -674,8 +674,8 @@
     any-cl : (i : ℕ) → (cl : List C) → Set
     any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl
 
-    n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
-    n<ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le  → clist-any n j le ) where
+    n≤ca-list : (n : ℕ) → n ≤ ca-list (clist (c n))
+    n≤ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le  → clist-any n j le ) 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)
@@ -700,14 +700,14 @@
               → suc (ca-list (del i cl a)) ≡ ca-list cl
          del-ca i cl a = a-list-ca i cl (a i ≤-refl) 
 
-         lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl
+         lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i ≤ ca-list cl
          lem30 0 cl i≤n a = begin
-             1 ≤⟨ s≤s z≤n ⟩ 
-             suc (ca-list (del 0 cl a) )  ≡⟨ del-ca 0 cl a ⟩
-             ca-list cl ∎ where
+            0 ≤⟨ z≤n ⟩ 
+            suc (ca-list (del 0 cl a) )  ≡⟨ del-ca 0 cl a ⟩
+            ca-list cl ∎ where
                 open ≤-Reasoning
          lem30 (suc i) cl i≤n a = begin
-            suc (suc i)   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ 
+            suc i   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ 
             suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩ 
             ca-list cl ∎ where
                 open ≤-Reasoning
@@ -715,22 +715,23 @@
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
-           n<ca : n < count-A ac
+           n<ca : n ≤ count-A ac
 
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) }
+    lem02 n = record { ac = c n ; n<ca = subst (λ k → n ≤ k) (ca-list=count-A (c n)) (n≤ca-list n ) }
 
     record CountB (n : ℕ) : Set where
        field
           b : B
           cb : ℕ
           b=cn : fun← cn cb ≡ g b
-          cb=n : count-B cb ≡ suc n
+          cb=n : count-B cb ≡ n
 
-    lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
-    lem01 n i le = lem09 i (count-B i) le refl where
+    lem01 : (n i : ℕ) → n ≤ count-B i → CountB n
+    lem01 0 i le = ?
+    lem01 (suc n) i le = ? where -- lem09 (suc n) i (count-B i) ? ? where
         -- starting from 0, if count B i ≡ suc n, this is it
-        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
+        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB (suc n)
         lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq } 
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
@@ -738,37 +739,33 @@
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq} 
         ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
-        lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
-        lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        lem09 : (n i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB (suc n)
+        lem09 n 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
         ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
         ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0
         ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
         ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
-        lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        lem09 n (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
         ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
         ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq)
-        ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
+        ... | yes isb | record { eq = eq1 } = lem09 n i j lt (cong pred eq)
+        ... | no nisb | record { eq = eq1 } = lem09 n i (suc j) (≤-trans lt a≤sa) eq
 
     bton : B → ℕ
     bton b = count-B (fun→ cn (g b))
 
     ntob : (n : ℕ) → B
-    ntob n = CountB.b (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 0 = ?
-    biso (suc n) = begin  -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl
-        bton (ntob (suc n)) ≡⟨ ? ⟩
-        count-B (fun→ cn (g (CountB.b CB1))) ≡⟨ sym ( cong (λ k → count-B (fun→ cn k)) ( CountB.b=cn CB1)) ⟩
-        count-B (fun→ cn (fun← cn (CountB.cb CB1))) ≡⟨ ? ⟩
-        count-B (CountB.cb CB1) ≡⟨ CountB.cb=n CB1 ⟩
-        ? ≡⟨ ? ⟩
-        suc n ∎ where
+    biso n = begin  
+        bton (ntob (suc n)) ≡⟨ refl ⟩
+        count-B (fun→ cn (g (CountB.b CB))) ≡⟨ sym ( cong (λ k → count-B (fun→ cn k)) ( CountB.b=cn CB)) ⟩
+        count-B (fun→ cn (fun← cn (CountB.cb CB))) ≡⟨ ? ⟩
+        count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩
+        n ∎ where
            open ≡-Reasoning
            CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
-           CB1 = lem01 (suc n) (maxAC.ac (lem02 (suc n))) (≤-trans (maxAC.n<ca (lem02 (suc n))) (ca≤cb0 (maxAC.ac (lem02 (suc n)))) )
-
 
     biso1 : (b : B) → ntob (bton b) ≡ b
     biso1 b = ?