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

changeset 466:14b0e0aa6487

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, 22 Mar 2022 15:40:57 +0900
parents aba3d15ad45c
children c65cb6c07a38
files src/ODC.agda
diffstat 1 files changed, 18 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODC.agda	Tue Mar 22 12:10:15 2022 +0900
+++ b/src/ODC.agda	Tue Mar 22 15:40:57 2022 +0900
@@ -121,28 +121,33 @@
 
 record ZChain ( A : HOD ) (x : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
-      NOMAX : OD
-      Chain : OD
-      nomax : (y m : Ordinal) → def NOMAX y → y o< x → ¬ ( * y < * m )
-      chain : (y : Ordinal) → def Chain y → NOMAX == od od∅  → SUP A (* y) _<_
+      NOMAX : HOD
+      Chain : HOD
+      nomax : (y m : Ordinal) → odef NOMAX y → y o< x → ¬ ( * y < * m )
+      chain : (y : Ordinal) → odef Chain y → & NOMAX ≡ o∅  → SUP A (* y) _<_
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
-    → ( (x y z : HOD) → x < y → y < z → x < z )
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → SUP A B  _<_  )
     → Maximal A _<_ 
-Zorn-lemma {A} {_<_} 0<A ztrans SUP = {!!} where
+Zorn-lemma {A} {_<_} 0<A SUP = zorn01 (TransFinite ind (& A)) where
      HasGreater : Ordinal → HOD
      HasGreater m = record { od = record { def = λ x → odef A x ∧ (* m < * x) } ; odmax = & A ; <odmax = {!!} }
+     zorn01 : ZChain A (& A) _<_ → Maximal A _<_
+     zorn01 zc with is-o∅ ( & (ZChain.NOMAX zc) )
+     ... | yes _ = {!!}
+     ... | no not = record { maximal = minimal (ZChain.NOMAX zc) (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}
+         ; ¬maximal<x = λ x lt m<x → ZChain.nomax zc {!!} {!!} (x∋minimal (ZChain.NOMAX zc) (λ eq → not (=od∅→≡o∅ eq)) ) {!!} {!!}  }
      ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
-     ind x prev = {!!} where
-        zlemma01 : {!!}
-        zlemma01 with is-o∅ (& (HasGreater x))
-        ... | no _ = {!!}
-        ... | yes _ = {!!}
-     zchain : (x : Ordinal) → ZChain A x _<_
-     zchain x = TransFinite ind x
+     ind x prev with Oprev-p x
+     ... | yes ox with is-o∅ (& (HasGreater x))
+     ... | yes _ = record { NOMAX = {!!} ; nomax = {!!} ; Chain = {!!} ; chain = {!!} } where
+     ... | no _ = record { NOMAX = {!!} ; nomax = {!!} ; Chain = {!!} ; chain = {!!} } where
+     ind x prev | no ¬ox with trio< (& A) x
+     ... | tri< a ¬b ¬c = {!!}
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b c = {!!}
 
 open import zfc