# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658112652 -32400
# Node ID 3c42f0441bbccdc86f22fe04cb6311bc5256e0df
# Parent  97efa6b434c9c2094e4922010bde919d170c35e2
...

diff -r 97efa6b434c9 -r 3c42f0441bbc src/zorn.agda
--- a/src/zorn.agda	Sat Jul 16 17:30:43 2022 +0900
+++ b/src/zorn.agda	Mon Jul 18 11:50:52 2022 +0900
@@ -256,7 +256,7 @@
 
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
    field
-      y-init   : supf o∅  ≡ y
+      u>0      : o∅ o< u    -- ¬ ch-init
       au       : odef A u
       ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
       asup     : (x : Ordinal) → odef A (supf x)
@@ -744,6 +744,26 @@
              → 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)
+
+          uzc-mono : {b : Ordinal } → {ob<x : osuc b o< x }
+             → odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b → odef pchain b
+          uzc-mono {b} {ob<x} ⟪ ab , record { u = x=0 ; u<x = u<x ; uchain = ch-init .b fc } ⟫ = 
+               ⟪ ab , record { u = x=0 ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ 
+          uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case2 x=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
+          uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
+               ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00 (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where
+                   uzc01 : ZChain.supf (prev (osuc b) ob<x) u  ≡ psupf0 u
+                   uzc01 = ?
+                   uzc00 : ChainP A f mf ay psupf0 u b
+                   uzc00 = ?
+
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension ? where -- ¬ A ∋ p, just skip
@@ -759,16 +779,18 @@
                             * a < * b → odef pchain b
                 z18 {a} {b} za b<x ab P a<b with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
-                ... | case2 b=sup = ⟪ ab , record { u = UChain.u (proj2 z30) ; u<x = ? ; uchain = ? } ⟫ where
+                ... | case2 b=sup with za
+                ... | ⟪ aa , record { u = _ ; u<x = u<x ; uchain = ch-init .a fca } ⟫ = uzc-mono z30 where
                     ob<x : osuc b o< x
                     ob<x = ?
                     z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b
-                    z30 = ZChain.is-max (pzc _ ob<x) ? <-osuc  ab (case1 ?) a<b 
-
-                --⊥-elim ( ¬x=sup record { 
-                --      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) ? 
-                --          (IsSup.x<sup b=sup ? )  } ) 
-
+                    z30 = ZChain.is-max (pzc _ ob<x) ⟪ aa , record { u = _ ; u<x = case2 refl ; uchain = ch-init a fca } ⟫ <-osuc  ab (case1 ?) a<b 
+                ... | ⟪ aa , record { u = u ; u<x = case2 u=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
+                ... | ⟪ aa , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = uzc-mono z30 where
+                    ob<x : osuc b o< x
+                    ob<x = ?
+                    z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b
+                    z30 = ZChain.is-max (pzc _ ob<x) ⟪ aa , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup ? ? } ⟫ <-osuc  ab (case1 ?) a<b 
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay   z  } (λ x → ind f mf ay x   ) (& A)