Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1369:43471e03d6fe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 21 Jun 2023 14:46:51 +0900
parents e5e592584382
children 3bcff593255e
files src/bijection.agda
diffstat 1 files changed, 10 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Wed Jun 21 13:24:54 2023 +0900
+++ b/src/bijection.agda	Wed Jun 21 14:46:51 2023 +0900
@@ -685,17 +685,23 @@
          --  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.
          --
-         del : (i : ℕ) → (cl : List C) → any-cl (suc i) cl → List C   -- del 0 contains ani 0
+         del : (i : ℕ) → (cl : List C) → any-cl i cl → List C   -- del 0 contains ani 0
          del = ?
-         del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del i cl a )
+         del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del (suc i) cl a )
          del-any = ?
-         del-ca : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl  )
+         del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl  )
               → suc (ca-list cl) ≡ ca-list (del i cl a)
          del-ca = ?
          lem06 : suc n < ca-list (clist (c (suc n)))
          lem06 = lem31 where
             lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl
-            lem30 0 cl i≤n a = ?
+            lem30 0 cl i≤n a = begin
+                2 ≤⟨ s≤s (s≤s z≤n) ⟩ 
+                suc (suc (ca-list (del 1 (del 0 cl a) ?) ))  ≡⟨ ? ⟩ 
+                suc (ca-list (del 1 cl ?) )  ≡⟨ ? ⟩ 
+                ca-list cl ∎ where
+                   open ≤-Reasoning
+            -- <-transʳ ? (subst (λ k → ca-list (del ? cl ?) < k) (a-list-ca ? ? (a _ ≤-refl))  a<sa )
             lem30 (suc i) cl i≤n a = begin
                suc (suc (suc i))   ≤⟨ s≤s (lem30 i (del (suc i) cl  a  ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ 
                suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩