# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658160905 -32400
# Node ID ac6b4d200f27588920accb2a8ac615de0df8abe4
# Parent  e864471a818fb8d6c8e5768fa2da03182a95f7ce
...

diff -r e864471a818f -r ac6b4d200f27 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 18 21:50:17 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 01:15:05 2022 +0900
@@ -209,6 +209,14 @@
       ... | case1 y=x = <-irr (case1 ( fcn-inject s mf cy cx  y=x ))  x<y
       ... | case2 y<x = <-irr (case2 x<y) (fcn-< s mf cy cx y<x ) 
 
+fc-conv : (A : HOD ) (f : Ordinal → Ordinal) {b u : Ordinal } 
+      →  {p0 p1 : Ordinal → Ordinal}
+      →  p0 u ≡ p1 u
+      →  FClosure A f (p0 u) b → FClosure A f (p1 u) b 
+fc-conv A f {.(p0 u)} {u}  {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) 
+       ( init (subst (λ k → odef A k) p0u=p1u ap0u ))
+fc-conv A f {_} {u}  {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv A f {_} {u}  {p0} {p1} p0u=p1u fc)
+
 -- open import Relation.Binary.Properties.Poset as Poset
 
 IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
@@ -425,7 +433,20 @@
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
      SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
-        zc1 x prev = {!!} where
+        zc1 x prev = record { is-max = is-max ; chain-mono2 = ? ; b<x→chain = ? } where
+           bchain : {b : Ordinal} → b o< x →
+                odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b →
+                odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+           bchain {b} b<x ⟪ ab , record { u = u ; u<x = u=0 ; uchain = ch-init b fc } ⟫ = 
+                  ⟪ ab , record { u = u ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ 
+           bchain {b} b<x ⟪ ab , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } ⟫ =  
+                  ⟪ ab , record { u = u ; u<x = case1 (b01 fc) ; uchain = ch-is-sup is-sup fc } ⟫ where
+               b01 : {b : Ordinal } → FClosure A f (ZChain.supf zc u) b → u o< x
+               b01 (init as) = ?
+               b01 (fsuc z fc) = b01 fc
+           chain-mono2 :  {a b c : Ordinal} → a o≤ b → b o≤ x →
+                odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
+           chain-mono2 {a} {b} {c} a≤b b≤x uac = ?
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
@@ -449,7 +470,7 @@
                  ... | tri> ¬a ¬b c = {!!}
            ... | no  lim = ZChain1.chain-mono2 (prev b b<x ) ? {!!} m04  where
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                    m04 = ZChain1.is-max (prev (osuc b) ? ) {!!} {!!} ab {!!} a<b
+                    m04 = ZChain1.is-max (prev (osuc b) ? ) {!!} <-osuc ab {!!} a<b
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -695,13 +716,6 @@
              → UnionCF A f mf ay psupf x ≡ pchain 
           chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 
-          fc-conv : {b u : Ordinal } 
-              →  {p0 p1 : Ordinal → Ordinal}
-              →  p0 u ≡ p1 u
-              →  FClosure A f (p0 u) b → FClosure A f (p1 u) b 
-          fc-conv {.(p0 u)} {u}  {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) ( init (subst (λ k → odef A k) p0u=p1u ap0u ))
-          fc-conv {_} {u}  {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv {_} {u}  {p0} {p1} p0u=p1u fc)
-
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension where -- ¬ A ∋ p, just skip