# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658213809 -32400
# Node ID 961abb22f2d9bc8a1d4bdb26ee5ca336df963c5c
# Parent  3c3e3a1291bb11e578c091ec2950a03891343bb8
...

diff -r 3c3e3a1291bb -r 961abb22f2d9 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 19 15:14:50 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 15:56:49 2022 +0900
@@ -478,12 +478,20 @@
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
                  ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
+                    m02 : (UChain.u (proj2 ua) o< px) ∨ (UChain.u (proj2 ua) ≡ o∅)
+                    m02 with UChain.u<x (proj2 ua)
+                    ... | case2 u=0 = case2 u=0
+                    ... | case1 u<x with trio< (UChain.u (proj2 ua))  px
+                    ... | tri< a ¬b ¬c = case1 a
+                    ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → _ o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫) --    u<x px<u
+                    ... | tri≈ ¬a b ¬c = ?  -- u = px case
+                    ---   if u = px, x is sup    px ≡ u < a < b o< x,   b ≡ px ∨ b o< a
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
-                    m03 = ?
+                    m03 = ⟪ proj1 ua , record { u = UChain.u (proj2 ua)  ; u<x = m02 ; uchain = UChain.uchain (proj2 ua) } ⟫
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = {!!}
+                 ... | tri≈ ¬a b=px ¬c = {!!}   -- b = px case
         ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x  }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -492,7 +500,7 @@
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x ? o≤-refl m04 where
                  m05 : b ≡ ZChain.supf zc b
-                 m05 = sym (ZChain.sup=u ? ab is-sup)
+                 m05 = sym (ZChain.sup=u ? ab is-sup)   -- ZChain on x
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup ? (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
 
@@ -561,7 +569,7 @@
 
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
      inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
-      ; initial = isy ; f-next = inext ; f-total = itotal ; chain<A = {!!} } where
+      ; initial = isy ; f-next = inext ; f-total = itotal ; chain<A = ? ; sup=u = ? } where
           isupf : Ordinal → Ordinal
           isupf z = y
           cy : odef (UnionCF A f mf ay isupf o∅) y
@@ -632,7 +640,7 @@
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
-          no-extension = record { supf = {!!} ; initial = pinit ; chain∋init = pcy 
+          no-extension = record { supf = ZChain.supf (prev px ? ); initial = pinit ; chain∋init = pcy 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
@@ -728,17 +736,17 @@
           ... | tri> ¬a ¬b c = spu
 
 
-          chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
-          chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = 
-                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ 
-          chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ = 
-                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} {!!} } ⟫ 
-          chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = 
-                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} (fsuc x {!!}) } ⟫ 
+          -- chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
+          -- chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = 
+          --          ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ 
+          -- chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ = 
+          --          ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} {!!} } ⟫ 
+          -- chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = 
+          --          ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} (fsuc x {!!}) } ⟫ 
           
-          chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
-             → UnionCF A f mf ay psupf x ≡ pchain 
-          chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
+          -- chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
+          --    → UnionCF A f mf ay psupf x ≡ pchain 
+          -- chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)