# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658364016 -32400
# Node ID dc208a885e0c5d77d1318398ac752f7792931e4a
# Parent  d92ad9e365b60b65303f528e3a2a300390684441
...

diff -r d92ad9e365b6 -r dc208a885e0c src/zorn.agda
--- a/src/zorn.agda	Thu Jul 21 09:03:28 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 09:40:16 2022 +0900
@@ -464,7 +464,7 @@
                 ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc) 
         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 with Oprev-p x
-        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x } where
+        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where
            px = Oprev.oprev op
            zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
            zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
@@ -595,7 +595,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 = ? ; sup=u = ? } where
+      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           isupf : Ordinal → Ordinal
           isupf z = y
           cy : odef (UnionCF A f mf ay isupf o∅) y
@@ -663,13 +663,26 @@
           pcy : odef pchain y
           pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
+          supf0 = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
-          no-extension = record { supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
-               ; initial = pinit ; chain∋init = pcy  ; sup=u = ? 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
-
+          no-extension = record { supf = supf0
+               ; initial = pinit ; chain∋init = pcy  ; sup=u = sup=u 
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ;  order = order } where
+              sup=u :  {b : Ordinal} {ab : odef A b} → b o< x 
+                    → IsSup A (UnionCF A f mf ay supf0 x) ab 
+                    → supf0 b ≡ b
+              sup=u {b} b<x is-sup with trio< b px
+              ... | tri< a ¬b ¬c = ZChain.sup=u zc a ?
+              ... | tri≈ ¬a refl ¬c = ?
+              ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
+              order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
+              order {b} {s} {z1} b<x s<b fc with trio< b px 
+              ... | tri< a ¬b ¬c = ZChain.order zc a s<b fc
+              ... | tri≈ ¬a refl ¬c = ?
+              ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
 
           chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
           chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
@@ -692,7 +705,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  supf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
-                     ; initial = pinit ; chain∋init  = pcy ; sup=u = ? } 
+                     ; initial = pinit ; chain∋init  = pcy ; sup=u = ? ; order = ? } 
           ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
      ... | no lim = zc5 where
 
@@ -741,7 +754,7 @@
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; sup=u = ?}
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; sup=u = ? ; order = ? }
 
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal
@@ -759,7 +772,7 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ?
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ? ; order = ?
               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x