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

changeset 1330:27ce91231127

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 Tue, 13 Jun 2023 11:47:55 +0900
parents 75894c1665f7
children 97ea311161ba
files src/bijection.agda
diffstat 1 files changed, 15 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Tue Jun 13 11:22:05 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 11:47:55 2023 +0900
@@ -778,29 +778,22 @@
          flen =  Data.List.Fresh.length 
          len=n : flen (FLany.flist fa) ≡ suc n
          len=n = ?
-         fli : FL fm → ℕ
+         fli : {n : ℕ } → FL n → ℕ
          fli (ca<n i x) = i
-         flist-top : (fl : FList fm) → 0 < flen fl  → ℕ
-         flist-top [] ()
-         flist-top (cons (ca<n i x₁) fl x) _ = fun→ cn (g (f (fun← an i)))
-         flist-2nd : (fl : FList fm) → 1 < flen fl  → ℕ
-         flist-2nd [] ()
-         flist-2nd (cons (ca<n i x₁) [] x) (s≤s ()) --  = fun→ cn (g (f (fun← an i)))
-         flist-2nd (cons (ca<n i ai<m) (cons j fl frj) fri) (s≤s 0<fl) = fun→ cn (g (f (fun← an (fli j))))
-         flist-last : (fl : FList fm) → 0 < flen fl  → ℕ
-         flist-last (cons i [] x) 0<fl = fun→ cn (g (f (fun← an (fli i))))
-         flist-last (cons i (cons j fl x) y) 0<fl = flist-last (cons j fl x) cl04 where
-             cl04 : 0 < flen (cons j fl x) 
-             cl04 = ≤-trans (s≤s z≤n) a<sa
-         cl00 : (fl : FL fm) → suc (count-A (fli fl)) ≡ count-A (suc (fli fl))
-         cl00 = ?
-         cl01 : (fl : FList fm) → (1<fl : 1 < flen fl ) → flist-top fl (<-trans a<sa 1<fl) < flist-2nd fl 1<fl
-         cl01 = ?
-         n<ca : (fl : FList fm) → flen fl ≤ count-A (flist-last fl ? )
-         n<ca [] = z≤n
-         n<ca (cons (ca<n i fi<fm) fl fr) = ? where
-             cl02 : flen fl ≤ count-A (flist-last fl ? )
-             cl02 = n<ca fl 
+         c : {n : ℕ} → (fl : FList n) → (i : ℕ) → i < flen fl  → ℕ
+         c (cons i [] x) j <fl = fli i
+         c (cons i (cons j fl x) y) zero 0<fl = fun→ cn (g (f (fun← an (fli j))))
+         c (cons i (cons j fl x) y) (suc k) 0<fl = c (cons j fl x) k cl04 where
+             cl04 : k < flen (cons j fl x) 
+             cl04 = ? -- ≤-trans (s≤s z≤n) a<sa
+         n<ca : (fl : FList fm) → (i : ℕ) → i ≤ flen fl → i + count-A (c fl 0 ?) ≤ count-A (c fl i ? )
+         n<ca [] i i<fl = ?
+         n<ca (cons (ca<n j fi<fm) fl fr) zero i<fl = ? 
+         n<ca (cons (ca<n j fi<fm) fl fr) (suc i) i<fl = cl03 where
+             cl02 : i + count-A (c fl 0 ?) ≤ count-A (c fl i ? )
+             cl02 = n<ca fl i ?
+             cl03 : (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 ?) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? )
+             cl03 = ?
 
 
     record CountB (n : ℕ) : Set where