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

changeset 1351:4c9ec06aafeb

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, 18 Jun 2023 12:16:29 +0900
parents 575777026a72
children bb4cd8035383
files src/bijection.agda
diffstat 1 files changed, 17 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jun 18 11:37:00 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 12:16:29 2023 +0900
@@ -922,12 +922,25 @@
          ... | tri> ¬a ¬b c₁ = a≤sa
          ... | tri≈ ¬a bi ¬c = ≤-refl
          lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
-         ... | tri≈ ¬a bi ¬c = ?
+         ... | tri≈ ¬a bi ¬c = lem02 i ≤-refl where
+             lem02 : (j : ℕ) → j ≤ i → suc (c1 j 0) ≤ 1
+             lem02 zero j≤i with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+             ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ z≤n a<sa  ))
+             ... | tri> ¬a ¬b c₁ = ≤-refl
+             lem02 (suc j) j≤i with <-cmp (fun→ cn (g (f (fun← an (suc j))))) zero
+             ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ j≤i a<sa  ))
+             lem02 (suc j) (s≤s j≤i) | tri> ¬a ¬b c₁ = lem02 j (≤-trans j≤i a≤sa)
          lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
     c1<count-A zero (suc i) = ?
-    c1<count-A (suc n) (suc i) with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
-    ... | no nisa | t = ?
-    ... | yes isa | t = ?
+    c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
+    ... | no nisa | tri< a ¬b ¬c = ? where
+          lem10 : c1 n (suc i) ≤ count-A (suc i)
+          lem10 = c1<count-A n (suc i)
+    ... | no nisa | tri≈ ¬a b ¬c = ?
+    ... | no nisa | tri> ¬a ¬b c₁ = ?
+    ... | yes isa | tri< a ¬b ¬c = ?
+    ... | yes isa | tri≈ ¬a b ¬c = ?
+    ... | yes isa | tri> ¬a ¬b c₁ = ?
 
     record maxAC (n : ℕ) : Set where
        field