# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649740244 -32400
# Node ID 5b1cfaf4c4ffe24703892d6dd9857abf3e16ecc5
# Parent  8ec0b88b022fd44e0bbe8207767158fe94d5a40e
...

diff -r 8ec0b88b022f -r 5b1cfaf4c4ff src/zorn.agda
--- a/src/zorn.agda	Tue Apr 12 10:22:15 2022 +0900
+++ b/src/zorn.agda	Tue Apr 12 14:10:44 2022 +0900
@@ -131,16 +131,30 @@
 
 -- finite IChain
 
-record InFiniteIChain {A : HOD} (x : Element A) : Set (suc n) where
+record InFiniteIChain {A : HOD} (x : Element A) (z : Ordinal) : Set (suc n) where
    field
-      y : Element A
-      y>x : IChainSet x ∋ elm y → elm x < elm y
+      ny : (y : Element A ) → & (elm y) o< z → Element A
+      y>x : {y : Element A} → (lt : & (elm y) o< z )→ IChainSet x ∋ elm y → elm y < elm (ny y lt )
       
 Zorn-lemma-case : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
-    → (x : Element A) → Sup> x ∨ Dec ( InFiniteIChain x )
-Zorn-lemma-case {A}  0<A PO x = {!!}
+    → (x : Element A) → Sup> x ∨ Dec ( InFiniteIChain x (& A))
+Zorn-lemma-case {A}  0<A PO x = zc2 where
+    Gtx : HOD
+    Gtx = record { od = record { def = λ y → odef ( IChainSet x ) y ∧  ( & (elm x) o< y ) } ; odmax = & A
+        ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 (proj1 lt))))  }
+    zc2 :  Sup> x ∨ Dec (InFiniteIChain x (& A))
+    zc2 with  is-o∅ (& Gtx)
+    ... | no not = case1 record { y = record { elm = ODC.minimal O Gtx (λ eq → not (=od∅→≡o∅ eq) ); is-elm = {!!} }  ; y>x = {!!} }
+    ... | yes nogt = case2 {!!} where
+        zc3 : {y : Element A} → IChainSet x ∋ elm y → ¬ (& (elm x) o< & (elm y))
+        zc3 = {!!}
+        zcind : (z : Ordinal ) → ((y : Ordinal) → y o< z → Dec (InFiniteIChain x y ) ) → Dec (InFiniteIChain x z)
+        zcind z prev = {!!}
+        zc4 : Dec (InFiniteIChain x (& A))
+        zc4 = TransFinite zcind (& A)
+
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A