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

changeset 1350:575777026a72

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 11:37:00 +0900
parents f5048a51d19f
children 4c9ec06aafeb
files src/bijection.agda
diffstat 1 files changed, 25 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jun 18 06:00:57 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 11:37:00 2023 +0900
@@ -899,12 +899,31 @@
     ... | yes isa | tri≈ ¬a b ¬c = ≤-refl
     ... | yes isa | tri> ¬a ¬b c₁ = a≤sa
     c1<count-A (suc n) zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
-    ... | no nisa | s = ?
-    ... | yes isa | tri≈ ¬a b ¬c = ? where
-         -- only one a in c1 n loop
-         lem00 : c1 n zero ≤ count-A zero
-         lem00 = c1<count-A n zero
-    ... | yes isa | tri> ¬a ¬b c₁ = ?
+    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b ) } )
+    ... | no nisa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
+         lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 0
+         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+         ... | tri> ¬a ¬b c₁ = ≤-refl
+         ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
+         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
+         ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an (suc i) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
+         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
+    ... | yes isa | tri≈ ¬a b ¬c = lem01 n ≤-refl where
+         lem01 : (i : ℕ) → i ≤ n → suc (c1 i 0) ≤ 1 
+         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+         ... | tri> ¬a ¬b c₁ = ≤-refl 
+         ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa  ))
+         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
+         ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa  ))
+         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
+    ... | yes isa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
+         lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 1 
+         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+         ... | 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 = ?
+         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 = ?