# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650603391 -32400
# Node ID 90f61d55cc547e1550e0bc1422e161a6b42878da
# Parent  5ca59261a4aaae406a39f8eba42dae42d9dd742c
...

diff -r 5ca59261a4aa -r 90f61d55cc54 src/zorn.agda
--- a/src/zorn.agda	Fri Apr 22 13:20:57 2022 +0900
+++ b/src/zorn.agda	Fri Apr 22 13:56:31 2022 +0900
@@ -469,22 +469,35 @@
      HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) →  odef A m → ¬ (* x < * m)) }  ; odmax = & A ; <odmax = z07 } where
          z07 :   {y : Ordinal} → odef A y ∧ ((m : Ordinal) → odef A m → ¬ (* y < * m)) → y o< & A
          z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
+     no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
+     no-maximum nomx x P = ¬x<0 (eq→ nomx {x} ? ) 
+     Gtx : { x : HOD} → A ∋ x → HOD
+     Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = {!!} } 
      cf : ¬ Maximal A → Ordinal → Ordinal
-     cf  = {!!}
+     cf  nmx x with ODC.∋-p O A (* x)
+     ... | no _ = o∅
+     ... | yes ax with is-o∅ (& ( Gtx ax ))
+     ... | yes nogt = ⊥-elim (no-maximum ? x x-is-maximal ) where -- no larger element, so it is maximal
+          x-is-maximal :  (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
+          x-is-maximal m am  = ⟪ subst (λ k → odef A k) &iso ax ,  ¬x<m  ⟫ where
+              ¬x<m :  ¬ (* x < * m)
+              ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
+     ... | no not =  & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
      cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
-     cf-is-<-monotonic = {!!}
+     cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
-     cf-is-≤-monotonic = {!!}
-     zsup : ZChain A sa (& A) → ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f  → Ordinal
-     zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )  ) )
-     A∋zsup : (zc : ZChain A sa (& A)) →  (nmx : ¬ Maximal A )  →  A ∋ * (zsup zc (cf nmx) (cf-is-≤-monotonic nmx))
-     A∋zsup zc nmx = {!!}
-     z03 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → f (zsup zc f mf ) ≡ zsup zc f mf 
+     cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
+     zsup : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f  → SUP A  (ZChain.chain zc) 
+     zsup zc f mf = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )   
+     -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )  ) )
+     A∋zsup : (zc : ZChain A sa (& A)) →  (nmx : ¬ Maximal A )  →  A ∋ * ( & ( SUP.sup (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) ))
+     A∋zsup zc nmx = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) )
+     z03 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → f (& ( SUP.sup (zsup zc f mf ))) ≡ & (SUP.sup (zsup zc f mf ))
      z03 = {!!}
      z04 : (zc : ZChain A sa (& A)) → ¬ Maximal A  → ⊥
-     z04 zc nmx = z01  {* (cf nmx c)} {* c} sa (A∋zsup zc nmx ) (case1 ( cong (*)( z03 zc (cf nmx) (cf-is-≤-monotonic nmx ))))
+     z04 zc nmx = z01  {* (cf nmx c)} {* c} {!!} (A∋zsup zc nmx ) (case1 ( cong (*)( z03 zc (cf nmx) (cf-is-≤-monotonic nmx ))))
            (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup zc nmx )))) where
-          c = zsup zc (cf nmx) (cf-is-≤-monotonic nmx)
+          c = & (SUP.sup (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)))
      -- ZChain is not compatible with the SUP condition
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa y ∨ Maximal A )
          →  ZChain A sa x ∨ Maximal A