# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670977178 -32400
# Node ID 4ce084a0dce2dcb8b16fc3790fba31db1a10e8cd
# Parent  5463f10d6843d6df2a9b73952647e7f280df6faf
supf-mono done

diff -r 5463f10d6843 -r 4ce084a0dce2 src/zorn.agda
--- a/src/zorn.agda	Tue Dec 13 19:58:13 2022 +0900
+++ b/src/zorn.agda	Wed Dec 14 09:19:38 2022 +0900
@@ -1235,8 +1235,8 @@
               mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
                  mf00 : * x < * (f x)
                  mf00 = proj1 ( mf< x ax )
-     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ?
-              ; zo≤sz = ?   ; is-minsup = ? ; cfcs = cfcs    }  where
+     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = 0<sufz
+              ; zo≤sz = ?   ; is-minsup = is-minsup ; cfcs = cfcs    }  where
 
           mf : ≤-monotonic-f A f
           mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
@@ -1293,6 +1293,20 @@
                     ZChain.supf (pzc oz<x) u  ≡⟨ su=u ⟩
                     u ∎ where open ≡-Reasoning 
 
+          chain⊆pchainU1 : {z w : Ordinal } → (z<x : z o< x) → odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim z<x))) z) w → odef pchainU w 
+          chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
+          chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ 
+             = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ  k → FClosure A f k w ) su=su fc) ⟫ where
+                 u<x : u o< x
+                 u<x = ordtrans u<oz z<x
+                 su=su : ZChain.supf (pzc (ob<x lim z<x)) u ≡ supfz u<x
+                 su=su = sym ( zeq _ _  (o<→≤ (osucc u<oz)) (o<→≤ <-osuc) )
+                 su≡u :  supfz u<x ≡ u
+                 su≡u = begin 
+                    ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩
+                    ZChain.supf (pzc (ob<x lim z<x)) u  ≡⟨ su=u ⟩
+                    u ∎ where open ≡-Reasoning 
+
           ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b }
             → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib)
             → IChain-i ia o< IChain-i ib
@@ -1429,17 +1443,25 @@
           ... | tri< y<x ¬b ¬c = zc01 where
                open o≤-Reasoning O
                zc01 : supf1 z o≤ 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 ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc)  ⟩
+               zc01 = begin
+                  supf1 z ≡⟨ sf1=sf (ordtrans≤-< z≤y y<x)  ⟩
+                  ZChain.supf (pzc  (ob<x lim (ordtrans≤-< z≤y y<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 ∎ 
-               ... | tri> ¬a ¬b c = ? -- y<x x o< z → ⊥ 
-               ... | tri≈ ¬a b ¬c with osuc-≡< ( subst (λ k → k o≤ y) b z≤y)
-               ... | case1 z=y = ? -- x=z=y ⊥
-               ... | case2 z<y = subst₂ (λ j k → j o≤ k ) ? refl ( MinSUP.minsup ssup ? ? )
-          ... | tri≈ ¬a b ¬c = ?
-          ... | tri> ¬a ¬b c = o≤-refl0 ? 
+          ... | tri≈ ¬a b ¬c = zc01 where  -- supf1 z o≤ spu
+               open o≤-Reasoning O
+               zc01 : supf1 z o≤ spu
+               zc01 with osuc-≡< (subst (λ k → z o≤ k) b z≤y)
+               ... | case1 z=x = o≤-refl0 (sf1=spu (sym z=x))
+               ... | case2 z<x = subst (λ k → k o≤ spu ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) 
+                 (MinSUP.as usup) (λ uw → MinSUP.x≤sup usup (chain⊆pchainU1 z<x uw)) )
+          ... | tri> ¬a ¬b c = zc01 where  -- supf1 z o≤ sps
+               zc01 : supf1 z o≤ sps
+               zc01 with trio< z x
+               ... | tri< z<x ¬b ¬c = IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) 
+                 (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 (chain⊆pchainU1 z<x uw)) )
+               ... | tri≈ ¬a z=x ¬c = MinSUP.minsup usup (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 uw) )
+               ... | tri> ¬a ¬b c = o≤-refl -- (sf1=sps 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))