# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650183383 -32400
# Node ID 5d3df69d3732b7edb736ca44da1577e6ee7de1ca
# Parent  5e364d55bccced1c5d904dde09f9cfbf00e3db11
zc10

diff -r 5e364d55bccc -r 5d3df69d3732 src/zorn.agda
--- a/src/zorn.agda	Sun Apr 17 16:03:29 2022 +0900
+++ b/src/zorn.agda	Sun Apr 17 17:16:23 2022 +0900
@@ -129,7 +129,7 @@
 ic→odef {A} {ox} (ifirst ax) = ax
 ic→odef {A} {ox} (inext ax x<y ic) = ax
 
-ic→< :  {A : HOD} → (IsPartialOrderSet A) → (x : Ordinal) → odef A x → {y : Ordinal} → (iy : IChain A y) → ic-connect {A} {y} x iy → * x < * y
+ic→< :  {A : HOD} → IsPartialOrderSet A → (x : Ordinal) → odef A x → {y : Ordinal} → (iy : IChain A y) → ic-connect {A} {y} x iy → * x < * y
 ic→< {A} PO x ax {y} (ifirst ay) ()
 ic→< {A} PO x ax {y} (inext ay x<y iy) (case1 refl) = x<y
 ic→< {A} PO x ax {y} (inext {oy} ay x<y iy) (case2 ic) = IsStrictPartialOrder.trans PO 
@@ -148,6 +148,12 @@
 IChainSet⊆A :  {A : HOD} → (x : Element A ) → IChainSet x ⊆ A
 IChainSet⊆A {A} x = record { incl = λ {oy} y → proj1 y }
 
+¬IChained-refl : (A : HOD) {x : Ordinal} → IsPartialOrderSet A → ¬ IChained A x x
+¬IChained-refl A {x} PO record { iy = iy ; ic = ic } = IsStrictPartialOrder.irrefl PO
+        {me (subst (λ k → odef A k ) (sym &iso) ic0) } {me (subst (λ k → odef A k ) (sym &iso) ic0) } refl (ic→< {A} PO x ic0 iy ic )  where
+     ic0 : odef A x
+     ic0 = ic→odef {A} iy
+
 -- there is a y, & y > & x
 
 record OSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
@@ -335,19 +341,30 @@
                 (subst (λ k → ic-connect (& k) (IChained.iy (proj2 zc5)) ) (me-elm-refl A x) (IChained.ic (proj2 zc5)) )  )
             zc6 : elm x < z
             zc6 = IsStrictPartialOrder.trans PO {x} {me (proj1 zc3)} {me az} zc7 y<z
-    ... | yes inifite = case2 (case2 record {    c-infinite = zc9 ; chain<x = {!!}} ) where
+    ... | yes inifite = case2 (case2 record {    c-infinite = zc9 ; chain<x = zc10} ) where
         B : HOD
         B = IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))
         Nx : (y : Ordinal) → odef A y → HOD
         Nx y ay = record { od = record { def = λ x → odef A x ∧ ( * y < * x ) } ; odmax = & A
               ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A (proj1 lt)))  }
+        zc10 : (oy : Ordinal) → odef (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) oy → oy o< & (elm x)
+        zc10 oy icsy = zc21 where
+             zc20 : (y : HOD) → (IChainSet x) ∋ y  → & (elm x) o< & y → ⊥
+             zc20 y icsy lt = ¬A∋x→A≡od∅ Gtx ⟪ icsy , lt ⟫ nogt
+             zc22 : IChainSet x ∋ * oy
+             zc22 = ⟪ subst (λ k → odef A k) (sym &iso) (proj1 icsy)
+                 , subst₂ (λ j k → IChained A j k) (cong (&) (me-elm-refl A x))  (sym &iso) (proj2 icsy)  ⟫
+             zc21 : oy o< & (elm x) 
+             zc21 with trio< oy (& (elm x) )
+             ... | tri< a ¬b ¬c = a
+             ... | tri≈ ¬a b ¬c = ⊥-elim (¬IChained-refl A PO (subst₂ (λ j k → IChained A j k ) zc23 b (proj2 icsy)) ) where
+                 zc23 : & (* (& (elm x))) ≡ & (elm x)
+                 zc23 = cong (&) *iso 
+             ... | tri> ¬a ¬b c = ⊥-elim ( zc20 (* oy) zc22 (subst (λ k → & (elm x) o< k) (sym &iso) c ))
         zc9 : (y : Ordinal) (cy : odef B y) →
             IChainSup> A (ic→A∋y A (subst (OD.def (od A)) (sym &iso) (is-elm x)) cy)
-        zc9 y cy with  ODC.∋-p O B (* y)
-        ... | no not = ⊥-elim (not (subst (λ k → odef B k ) (sym &iso) cy))
-        ... | yes cy1  with is-o∅ (& (Nx y (proj1 cy) ))
+        zc9 y cy with is-o∅ (& (Nx y (proj1 cy) ))
         ... | yes no-next = ⊥-elim zc16 where
-             -- cy      : OD.def (od A) y ∧ IChained A (& (* (& (elm x)))) y
              zc18 :  ¬ IChainSup> A (subst (odef A) (sym &iso) (proj1 (subst (λ k → odef (IChainSet (me (d→∋ A (is-elm x)))) k) (sym &iso) cy)))
              zc18 ics = ¬A∋x→A≡od∅ (Nx y (proj1 cy) ) ⟪ subst (λ k → odef A k ) (sym &iso) (IChainSup>.A∋y ics)
                   ,  subst₂ (λ j k → j < k ) *iso (cong (*) (sym &iso))( IChainSup>.y>x ics) ⟫ no-next