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

diff -r 9a85233384f7 -r ce713b5db3f3 src/zorn.agda
--- a/src/zorn.agda	Mon Nov 14 07:35:18 2022 +0900
+++ b/src/zorn.agda	Wed Nov 16 14:11:28 2022 +0900
@@ -696,20 +696,16 @@
         zc1 x prev with Oprev-p x  
         ... | yes op = record { is-max = is-max ; order = order  } where
                px = Oprev.oprev op
-               zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
-               zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
                   b o< x → (ab : odef A b) →
                   HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
                   * a < * b → odef (UnionCF A f mf ay supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-               is-max {a} {b} ua b<x ab P a<b | case2 is-sup
-                 = ⟪ ab , ch-is-sup b sb<sx  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
+               ... | case2 sb<sx = ⟪ ab , ch-is-sup b sb<sx  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
                   b<A : b o< & A
                   b<A = z09 ab
-                  sb<sx : supf b o< supf x
-                  sb<sx  = ? 
                   m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
                   m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                         chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
@@ -722,6 +718,20 @@
                   m09 {s} {z} s<b fcz = order b<A s<b fcz
                   m06 : ChainP A f mf ay supf b
                   m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
+               ... | case1 sb=sx = ? where
+                  m09 : IsSUP A (UnionCF A f mf ay (ZChain.supf zc) b) ab
+                  m09 = proj2 is-sup
+                  m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                  m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
+                        chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
+                  m05 : ZChain.supf zc b ≡ b
+                  m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+
+                  m07 : MinSUP A (UnionCF A f mf ay supf (supf x)) -- supf z o< supf ( supf x )
+                  m07 = ZChain.minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
+                  m08 : MinSUP A (UnionCF A f mf ay supf b)
+                  m08 = ZChain.minsup zc (o<→≤ (z09 ab))           -- supf z o< supf b
+
         ... | no lim = record { is-max = is-max ; order = order }  where
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
                   b o< x → (ab : odef A b) →