# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647931257 -32400
# Node ID 14b0e0aa64879b1630bde002a7eafb97332e7ce4
# Parent  aba3d15ad45cb4cf027ab2b0181f79cb4817004d
...

diff -r aba3d15ad45c -r 14b0e0aa6487 src/ODC.agda
--- 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