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

changeset 519:ef5dde91fa80

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 Sat, 16 Apr 2022 18:52:48 +0900
parents fc16a22225d9
children 5e364d55bccc
files src/ODUtil.agda src/zorn.agda
diffstat 2 files changed, 17 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODUtil.agda	Sat Apr 16 18:14:48 2022 +0900
+++ b/src/ODUtil.agda	Sat Apr 16 18:52:48 2022 +0900
@@ -70,6 +70,9 @@
 ⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (incl FU (subst (λ k → odef F k) (sym &iso) lt) )
                                      ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (incl UF (subst (λ k → odef U k) (sym &iso) lt) ) }
 
+¬A∋x→A≡od∅ : (A : HOD) → {x : HOD} → A ∋ x  → ¬ ( & A ≡ o∅ )
+¬A∋x→A≡od∅ A {x} ax a=0 = ¬x<0 ( subst (λ k → & x o< k) a=0 (c<→o< ax ))
+
 subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
 subset-lemma  {A} {x} = record {
       proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
--- a/src/zorn.agda	Sat Apr 16 18:14:48 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 18:52:48 2022 +0900
@@ -345,15 +345,21 @@
         zc9 y cy with  ODC.∋-p O (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) (* y)
         ... | no not = ⊥-elim (not (subst (λ k → odef (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) k ) (sym &iso) cy))
         ... | yes cy1  with is-o∅ (& (Nx y (proj1 cy) ))
-        ... | yes no-next = {!!} 
+        ... | yes no-next = ⊥-elim zc16 where
+             zc18 : IChainSup> A (d→∋ A (is-elm x)) → ⊥
+             zc18 ics = ¬A∋x→A≡od∅ (Nx y (proj1 cy) ) ⟪ {!!} , ? ⟫ no-next  
+             zc17 : IsFC A {& (elm x)} (d→∋ A (is-elm x)) (& (* y))
+             zc17 = record { icf = cy ; c-finite = λ icsup → zc18 icsup }
+             zc16 : ⊥
+             zc16 = ¬A∋x→A≡od∅ HG ⟪ subst (λ k → odef A k ) (sym &iso) (proj1 cy ) , zc17 ⟫ inifite 
         ... | no not = record { y = zc14 ; A∋y = IChainSup>.A∋y (proj2 zc12) ; y>x = zc15 } where
-                  zc13 = ODC.minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
-                  zc12 : odef A (& zc13 ) ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) (proj1 cy) )
-                  zc12 = ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
-                  zc14 : Ordinal
-                  zc14 = IChainSup>.y (proj2 zc12) 
-                  zc15 : * y < * ( IChainSup>.y (proj2 (ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq)))) )
-                  zc15 = IChainSup>.y>x (proj2 zc12)
+             zc13 = ODC.minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
+             zc12 : odef A (& zc13 ) ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) (proj1 cy) )
+             zc12 = ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
+             zc14 : Ordinal
+             zc14 = IChainSup>.y (proj2 zc12) 
+             zc15 : * y < * ( IChainSup>.y (proj2 (ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq)))) )
+             zc15 = IChainSup>.y>x (proj2 zc12)
 
 all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
      → (( x : Element A) → OSup> A (d→∋ A (is-elm x) ))