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

changeset 1324:1eefc6600354

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 Sun, 11 Jun 2023 18:49:13 +0900
parents 95f6216499d7
children 8b909deb840e
files src/bijection.agda
diffstat 1 files changed, 27 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jun 11 17:15:12 2023 +0900
+++ b/src/bijection.agda	Sun Jun 11 18:49:13 2023 +0900
@@ -696,30 +696,36 @@
     fla-max< zero n i≤n = ?
     fla-max< (suc i) n i≤n = ?
 
-    record FLany (n m : ℕ ) : Set where
+    fla0 : (i n : ℕ ) → i < suc n → FList (fla-max n)
+    fla0 zero n lt = FLinsert fl0 []  where
+        fl0 : FL (fla-max n )
+        fl0 = ca<n zero (fla-max< zero n 0<s )
+    fla0 (suc i) n (s≤s lt) = FLinsert fl0 fl1  where
+        fl0 : FL (fla-max n )
+        fl0 = ca<n (suc i) (fla-max< (suc i) n ? )
+        fl1 = fla0 i n (≤-trans refl-≤s (s≤s lt)) 
+    fla : (n : ℕ) → FList (fla-max n)
+    fla n = fla0 n n a<sa  
+
+    record FLany (n : ℕ ) : Set where
        field
           flist  : FList (fla-max n)
-          flany  : (i : ℕ) → (i<n : i < suc m ) → (m≤n : suc m < suc n) → Any ( ca<n i (fla-max< i n (<-trans i<n m≤n )  ) ≡_) flist
+          flany  : (i : ℕ) → (i<n : i < suc n ) →  Any ( ca<n i (fla-max< i n i<n ) ≡_) flist
 
-    fla : (n : ℕ) → FLany n n
-    fla n = fla0 n a<sa  where
-        fla0 : (i : ℕ ) → i < suc n → FLany n i
-        fla0 zero lt = record { flist = FLinsert fl0 [] ; flany = fl1 } where
-             fl0 : FL (fla-max n )
-             fl0 = ca<n zero (fla-max< zero n 0<s )
-             fl1 : (i : ℕ) (i<n : i < 1) (m≤n : 1 < suc n) → Any (_≡_ (ca<n i (fla-max< i n (<-trans i<n m≤n)))) (FLinsert fl0 [])
-             fl1 zero (s≤s z≤n) lt = x∈FLins fl0 [] 
-        fla0 (suc i) (s≤s lt) = record { flist = FLinsert fl0 fl1 ; flany = fl2 } where
-             fl0 : FL (fla-max n )
-             fl0 = ca<n i (fla-max< i n (≤-trans lt refl-≤s ) )
-             fl1 = FLany.flist ( fla0 i (≤-trans refl-≤s (s≤s lt)) )
-             fl3 = x∈FLins fl0 fl1 
-             fl4 = FLany.flany (fla0 i (≤-trans refl-≤s (s≤s lt))) 
-             fl2 :  (j : ℕ) (i<n : j < suc (suc i)) (m≤n : suc (suc i) < suc n) 
-                  → Any (_≡_ (ca<n j (fla-max< j n (<-trans i<n m≤n)))) (FLinsert fl0 fl1)
-             fl2 j i<n m≤n with ≤-∨ i<n 
-             ... | case1 eq = ?
-             ... | case2 lt = ? -- fl4 ? ? ? -- FLany.flany ( fla0 i ? ) j ? ?
+    flany : (n : ℕ) → FLany n
+    flany n = record { flist = fla0 n n a<sa ; flany = ? } where
+        flany0  : (i : ℕ) → (i<n : i < suc n ) → Any ( ca<n i (fla-max< i n i<n ) ≡_) (fla0 i n i<n)
+        flany0 zero i<n = fl1 where
+            fl0 = ca<n zero (fla-max< zero n 0<s )
+            fl1 = x∈FLins fl0 [] 
+        flany0 (suc i) (s≤s i<n) = fl3 where
+            fl0 : FL (fla-max n )
+            fl0 = ca<n (suc i) (fla-max< (suc i) n ? )
+            fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n)) 
+            fl3 = x∈FLins fl0 fl1 
+            fl4  : Any ( ca<n i (fla-max< i n (≤-trans refl-≤s (s≤s i<n)) ) ≡_) (fla0 i n (≤-trans refl-≤s (s≤s i<n)))
+            fl4 = flany0 i (≤-trans refl-≤s (s≤s i<n)) 
+
  
     lem02 : (n : ℕ) → maxAC n
     lem02 n = lem03 n where