# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670924355 -32400
# Node ID 33d601c9ee96ca19e99eaf75453125572ac7d396
# Parent  99df080f4fdb3d72c23d95f1a36acb9c6876c8bf
...

diff -r 99df080f4fdb -r 33d601c9ee96 src/zorn.agda
--- a/src/zorn.agda	Tue Dec 13 09:31:11 2022 +0900
+++ b/src/zorn.agda	Tue Dec 13 18:39:15 2022 +0900
@@ -886,7 +886,8 @@
              m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz)
 
           zc41 : ZChain A f mf< ay x
-          zc41 =  record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order ; 0<supfz = ?
+          zc41 =  record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order 
+              ; 0<supfz = 0<supfz 
               ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ;  cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
@@ -939,6 +940,9 @@
                        zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
 
+                 0<supfz : {x : Ordinal } → o∅ o< supf1 x
+                 0<supfz = ordtrans<-≤ (ZChain.0<supfz zc) (OrdTrans (o≤-refl0 (sym (sf1=sf0 o∅≤z))) (supf1-mono o∅≤z))
+
                  sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
                  sf≤ {z} x≤z with trio< z px
                  ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
@@ -1448,15 +1452,18 @@
                zc01 : supf1 z o≤ supf1 y -- ZChain.supf (pzc  (ob<x lim y<x)) y
                zc01 with trio< z x
                ... | tri< z<x ¬b ¬c = begin
-                  ZChain.supf (pzc  (ob<x lim z<x)) z ≤⟨ ZChain.supf-mono (pzc  (ob<x lim z<x)) z≤y  ⟩
-                  ZChain.supf (pzc  (ob<x lim z<x)) y ≡⟨ zeq _ _ ? ? ⟩
-                  ZChain.supf (pzc  (ob<x lim y<x)) y ≡⟨ sym (sf1=sf ?) ⟩
+                  ZChain.supf (pzc  (ob<x lim z<x)) z ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc)  ⟩
+                  ZChain.supf (pzc  (ob<x lim y<x)) z ≤⟨ ZChain.supf-mono (pzc  (ob<x lim y<x)) z≤y  ⟩
+                  ZChain.supf (pzc  (ob<x lim y<x)) y ≡⟨ sym (sf1=sf y<x) ⟩
                   supf1 y ∎ 
                ... | tri≈ ¬a b ¬c = ?
                ... | tri> ¬a ¬b c = ?
           ... | tri≈ ¬a b ¬c = ?
           ... | tri> ¬a ¬b c = ?
 
+          0<sufz : {x : Ordinal } → o∅ o< supf1 x
+          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 = ?
 
@@ -1489,7 +1496,20 @@
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-               ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ?  ⟫
+               ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans zc45 su=u) zc44 ⟫ where
+                   u<b : u o< b
+                   u<b = osucprev ( begin
+                       osuc u ≤⟨ osucc u<x ⟩
+                       osuc m ≤⟨ osucc m<x ⟩
+                       x ≡⟨ sym b=x ⟩
+                       b ∎ ) where open o≤-Reasoning O
+                   zc45 : supf1 u ≡  ZChain.supf (pzc  (ob<x lim m<x)) u 
+                   zc45 = begin
+                       supf1 u ≡⟨ sf1=sf (subst (λ k → u o< k) b=x u<b )  ⟩
+                       ZChain.supf (pzc  (ob<x lim (subst (λ k → u o< k) b=x u<b ))) u  ≡⟨ zeq _ _ (osucc u<x) (o<→≤ <-osuc)  ⟩
+                       ZChain.supf (pzc  (ob<x lim m<x)) u ∎  where open ≡-Reasoning 
+                   zc44 : FClosure A f (supf1 u) w
+                   zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
@@ -1504,7 +1524,14 @@
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with zcb
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-               ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ?  ⟫
+               ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u u<x (trans zc45 su=u) zc44  ⟫ where
+                   zc45 : supf1 u ≡  ZChain.supf (pzc  (ob<x lim b<x)) u 
+                   zc45 = begin
+                       supf1 u ≡⟨ sf1=sf (ordtrans u<x b<x)  ⟩
+                       ZChain.supf (pzc  (ob<x lim (ordtrans u<x b<x) )) u  ≡⟨ zeq _ _ (o<→≤ (osucc u<x)) (o<→≤ <-osuc)  ⟩
+                       ZChain.supf (pzc  (ob<x lim b<x )) u ∎  where open ≡-Reasoning 
+                   zc44 : FClosure A f (supf1 u) w
+                   zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function