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

changeset 1367:f93ef96caeb7

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 12:23:58 +0900
parents 07fe8f8bb6d3
children e5e592584382
files src/bijection.agda
diffstat 1 files changed, 23 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Wed Jun 21 10:33:36 2023 +0900
+++ b/src/bijection.agda	Wed Jun 21 12:23:58 2023 +0900
@@ -759,25 +759,36 @@
              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 : (i : ℕ) → (cl : List C) → any-cl (suc i) cl → List C   -- del 0 contains ani 0
          del = ?
-         del-any : (i : ℕ) → i ≤ n → (cl : List C) → any-cl (suc i) cl  → any-cl i cl  
+         del-any : (i : ℕ) → (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 : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl  )
+              → suc (ca-list cl) ≡ ca-list (del i 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)
+         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 i cl i≤n a = begin
+               suc (suc i)  ≤⟨ ? ⟩ 
+               ca-list cl ∎ where
+                   open ≤-Reasoning
+            lem31 : suc n < ca-list (clist (c (suc n)))
+            lem31 = lem30 n (clist (c (suc n))) a≤sa (λ j le  → clist-any (suc n) j le )
+            lem07 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → i < ca-list (del i 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) 
+            lem07 (suc i) cl le a = sx≤py→x≤y ( begin
+                suc (suc (suc i)) ≤⟨ ? ⟩
+                suc (suc (ca-list cl)) ≡⟨ ? ⟩
+                ca-list (del (suc (suc i)) (del (suc i) cl a) ?)  ≡⟨ ? ⟩
+                suc (ca-list (del (suc i) cl a )) ∎ ) where
+                    open ≤-Reasoning
+                    lem08 : i < ca-list (del (suc i) cl a)                                           
+                    lem08 = lem07 i (del (suc i) cl a) (≤-trans a≤sa le) (del-any (suc i) 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
+            lem09 : any-cl (suc (suc n)) (clist (c (suc (suc n))))
+            lem09 i le = clist-any (suc (suc n)) i le
     n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
     n<ca-list n = ?