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

diff -r ef5dde91fa80 -r 5e364d55bccc src/zorn.agda
--- a/src/zorn.agda	Sat Apr 16 18:52:48 2022 +0900
+++ b/src/zorn.agda	Sun Apr 17 16:03:29 2022 +0900
@@ -169,6 +169,7 @@
 
 record InFiniteIChain (A : HOD) {x : Ordinal}  (ax : A ∋ * x) : Set n where
    field
+      chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
           → IChainSup> A (ic→A∋y A ax cy)
 
@@ -282,7 +283,7 @@
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field
       icy : odef (IChainSet {A} (me ax)) y  
-      c-finite : ¬ IChainSup> A ax
+      c-finite : ¬ IChainSup> A (subst (λ k → odef A k ) (sym &iso) (proj1 icy) )
       
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -326,7 +327,7 @@
         zc5 : odef (IChainSet {A} (me (d→∋ A (is-elm x) ))) (& y)
         zc5 = IsFC.icy (proj2 zc3)
         zc4 : {z : HOD} → A ∋ z → ¬ (y < z)
-        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; A∋y =  az ; y>x = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) zc6 } where
+        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; A∋y =  az ; y>x = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) y<z } where
             zc8 : ic-connect (& (* (& (elm x)))) (IChained.iy (proj2 zc5)) 
             zc8 = IChained.ic (proj2 zc5)
             zc7 : elm x < y
@@ -334,37 +335,35 @@
                 (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 } ) where
+    ... | yes inifite = case2 (case2 record {    c-infinite = zc9 ; chain<x = {!!}} ) 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 = λ y → odef A y ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) ay)  } ; odmax = & A
+        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)))  }
-        zc9 : (y : Ordinal) (cy : odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) y) →
+        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 (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))
+        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) ))
         ... | 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  
+             -- 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  
              zc17 : IsFC A {& (elm x)} (d→∋ A (is-elm x)) (& (* y))
-             zc17 = record { icf = cy ; c-finite = λ icsup → zc18 icsup }
+             zc17 = record { icy = subst (λ k → odef (IChainSet (me (d→∋ A (is-elm x)))) k ) (sym &iso) cy ; c-finite = zc18 }
              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
+        ... | no not = record { y = & zc13 ; A∋y = proj1 zc12  ; y>x = proj2 zc12 }  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 : odef A (& zc13 ) ∧ ( * y < * ( & zc13 ))
              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) ))
      → InFiniteIChain A (d→∋ A (ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ))
-all-climb-case {A} 0<A PO climb = record {    c-infinite = {!!}  } 
+all-climb-case {A} 0<A PO climb = record {    c-infinite = {!!}  ; chain<x = {!!} } 
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field