# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658734596 -32400
# Node ID 9aa0fc917100f66a46aa69c8b5d1883a60297228
# Parent  eb68d0870cc6c46fa581d177e80e33620bd92995
...

diff -r eb68d0870cc6 -r 9aa0fc917100 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 25 14:56:49 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 16:36:36 2022 +0900
@@ -494,23 +494,18 @@
                     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 = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
+                    b<A : b o< & A
+                    b<A = z09 ab
                     m05 : b ≡ ZChain.supf zc b
                     m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
-                    m04 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
-                    m04 {z} fcz with IsSup.x<sup is-sup ⟪ A∋fc y f mf fcz , ch-init fcz ⟫
-                    ... | case1 z=b = ?
-                    ... | case2 z<b = subst (λ k → z << k) m05 z<b
-                    m07 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                    m07 {sup1} s<b (init ay) with IsSup.x<sup is-sup ⟪ A∋fc y f mf (init ay) , ch-is-sup  ⟫
-                    ... | case1 z=b = ?
-                    ... | case2 z<b = subst (λ k → z << k) m05 z<b
-                    m07 {sup1} s<b (fsuc is-sup-z fcz) with IsSup.x<sup is-sup ⟪ A∋fc y f mf fcz , ch-is-sup  ⟫
-                    ... | case1 z=b = ?
-                    ... | case2 z<b = subst (λ k → z << k) m05 z<b
+                    m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z << ZChain.supf zc b
+                    m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
+                    m09 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+                    m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
                     m06 : ChainP A f mf ay (ZChain.supf zc) b b
                     m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) ; supfu=u = sym m05 
-                      ; fcy<sup = m04  ; order = ? }
+                      ; fcy<sup = m08  ; order = m09 }
         ... | no lim = record { is-max = is-max }  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) →
@@ -618,6 +613,7 @@
       ; 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 =  & (SUP.sup (ysup f mf ay))
+          sp = ysup f mf ay
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
           y<sup : * y ≤ SUP.sup (ysup f mf ay)
@@ -633,13 +629,16 @@
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb) 
-          imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a →
-            b o< o∅ → (ab : odef A b) →
-            HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
-            * a < * b → odef (UnionCF A f mf ay isupf o∅) b
-          imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
-          imax {a} {b} ua b<x ab (case2 sup)  a<b = ⊥-elim ( ¬x<0 b<x )
+               uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)  
+
+          csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z)
+          csupf {z} = ⟪ SUP.A∋maximal sp   , ch-is-sup o∅ o≤-refl uz02 (init ( SUP.A∋maximal sp))  ⟫ where
+               uz02 : ChainP A f mf ay isupf o∅ (isupf z)
+               uz02 = record { csupz = init (SUP.A∋maximal sp) ; supfu=u = ? ; fcy<sup = ? ; order = ? }
+               uz03 : {z : Ordinal} → FClosure A f y z → z << isupf o∅
+               uz03 = ? 
+               uz04 : {sup1 z1 : Ordinal} → sup1 o< o∅ → FClosure A f (isupf sup1) z1 → z1 << isupf o∅
+               uz04 = ?
 
      --
      -- create all ZChains under o< x