# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669260641 -32400
# Node ID eb2d0fb19b67623dc61df2e19af9aa03947b0d74
# Parent  c63f1fadd27f47ddb62ae7fc94565ec80751ae5e
...

diff -r c63f1fadd27f -r eb2d0fb19b67 src/zorn.agda
--- a/src/zorn.agda	Thu Nov 24 11:18:46 2022 +0900
+++ b/src/zorn.agda	Thu Nov 24 12:30:41 2022 +0900
@@ -529,11 +529,9 @@
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
        z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) 
                    (sym (supf-is-minsup b≤z)) 
-                   (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z ? fc )) where
+                   (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z (subst (λ k → k o< b) (sym (ChainP.supu=u is-sup)) u<b) fc )) where
                u<b : u o< b
                u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x )
-               su<z : supf u o< z
-               su<z = subst (λ k → k o< z ) (sym (ChainP.supu=u is-sup)) ( ordtrans<-≤ u<b b≤z )
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
@@ -858,8 +856,15 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
+                          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 ⟫
+                          m14 : ZChain.supf zc b o< x
+                          m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.cfcs zc mf< b<x x≤A ? fc
+                          m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
         ... | 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 →
@@ -896,8 +901,15 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
+                          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 ⟫
+                          m14 : ZChain.supf zc b o< x
+                          m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.cfcs zc mf< b<x x≤A ? fc
+                          m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -1169,7 +1181,9 @@
                           order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
                                    (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
                                    (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                       spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
+                                       spx≤px ss0<spx (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
+                                          ss0<spx : supf0 s o< spx 
+                                          ss0<spx = ?
                                           ss<px : supf0 s o< px
                                           ss<px = osucprev ( begin
                                             osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 ( begin
@@ -1471,8 +1485,6 @@
                fcb : FClosure A f (supfb a) w
                fcb = ?
                --  supfb a o≤ supfb b
-               sa<b : supfb a o< osuc b
-               sa<b = ?
                zcb : odef (UnionCF A f mf ay supfb b) w
                zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) ? fcb
                zc40 : odef (UnionCF A f mf ay supf1 b) w