# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670984476 -32400
# Node ID b3d69534077357feaa15fc97693056281be9e056
# Parent  4ce084a0dce2dcb8b16fc3790fba31db1a10e8cd
...

diff -r 4ce084a0dce2 -r b3d695340773 src/zorn.agda
--- a/src/zorn.agda	Wed Dec 14 09:19:38 2022 +0900
+++ b/src/zorn.agda	Wed Dec 14 11:21:16 2022 +0900
@@ -1467,7 +1467,23 @@
           0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z))
 
           is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
-          is-minsup = ?
+          is-minsup {z} z≤x with osuc-≡< z≤x
+          ... | case1 z=x = ?
+          ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
+               supf0 = ZChain.supf (pzc (ob<x lim z<x)) 
+               msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
+               msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc)
+               zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z 
+               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup  ⟪ az , ch-init fc ⟫ ) -- U supf0
+               zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) 
+                  ( IsMinSUP.x≤sup msup  ⟪ az , ch-is-sup u u<b ? ? ⟫ ) -- U supf0
+               zm01 : { s : Ordinal } → odef A s →  ( {x : Ordinal  } → odef (UnionCF A f ay supf1 z) x → x ≤ s )  → supf1 z o≤ s
+               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where -- U supf1
+                   zm02 : {w : Ordinal } →  odef (UnionCF A f ay supf0 z) w → w ≤ s
+                   zm02 {w} ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫
+                   zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup  ⟪ az , ch-is-sup u u<b ? ? ⟫
+
+
 
           cfcs :  {a b w : Ordinal } → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
           cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x