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

changeset 1359:88356bb882d4

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 Mon, 19 Jun 2023 12:40:47 +0900
parents 4eac5585b6b1
children e3d3749e80bd
files src/bijection.agda
diffstat 1 files changed, 6 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Mon Jun 19 12:33:23 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 12:40:47 2023 +0900
@@ -976,8 +976,12 @@
              ... | tri≈ ¬a b ¬c = ?
              ... | tri> ¬a ¬b c₁ = ?
              lem13 (suc j) j≤n with <-cmp (fun→ cn (g (f (fun← an (suc j))))) (suc i)
-             ... | tri< a ¬b ¬c = ?
-             ... | tri≈ ¬a b ¬c = ?
+             ... | tri< a ¬b ¬c = lem16 where
+                  lem16 : suc (suc (c1 j (suc i))) ≤ suc (count-A i)
+                  lem16 = ?
+                  lme14 : suc (c1 j (suc i)) ≤ suc (count-A i)
+                  lme14 = lem13 j ?
+             ... | tri≈ ¬a b ¬c = ? -- cong suc (lem13 j ?)
              ... | tri> ¬a ¬b c₁ = ?
        ... | tri≈ ¬a b ¬c = lem13 where  -- count-A contains (suc i) here
              lem15 : c1 n i ≡ c1 n (suc i)