# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670867941 -32400
# Node ID f24f4de4d459f57dd1edb14a17ad9937bcc12c05
# Parent  074b6a506b1b1922ebb5552eecdf6306ebbb30af
add 0<supfz

diff -r 074b6a506b1b -r f24f4de4d459 src/zorn.agda
--- a/src/zorn.agda	Tue Dec 13 00:14:32 2022 +0900
+++ b/src/zorn.agda	Tue Dec 13 02:59:01 2022 +0900
@@ -350,6 +350,7 @@
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
       zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x
+      0<supfz : {x : Ordinal } → o∅ o< supf x
 
       is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
 
@@ -885,7 +886,7 @@
              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
+          zc41 =  record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order ; 0<supfz = ?
               ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ;  cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
@@ -1238,14 +1239,14 @@
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-     ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) 
+     ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? 
               ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
               ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ?    } where
               mf : ≤-monotonic-f A f
               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 = ?
+     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ?
               ; zo≤sz = ?   ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
           -- mf : ≤-monotonic-f A f
@@ -1320,42 +1321,23 @@
                      ZChain.supf (pzc (pic<x ia)) (IChain-i ib)  ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ 
                      ZChain.supf (pzc (pic<x ia)) (IChain-i ia)  ∎ ) sa<sb ) where open o≤-Reasoning O
 
+          IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b )
+              → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a
+          IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫
+          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where
+               ic02 : o∅ o< supfz i<x 
+               ic02 = ZChain.0<supfz (pzc  (ob<x lim i<x)) 
+               ic01 : o∅ o< i
+               ic01 = ordtrans<-≤ ic02 sa<x
+          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib 
+              = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x)
+                  (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc )
+
           ptotalx : IsTotalOrderSet pchainx
-          ptotalx {a} {b} ia ib with trio< (ZChain.supf (pzc (pic<x (proj2 ia))) (IChain-i (proj2 ia)))  
-                                           (ZChain.supf (pzc (pic<x (proj2 ib))) (IChain-i (proj2 ib)))
-          ... | tri< ia<ib ¬b ¬c = uz01 where
-              uz01 : Tri (a < b) (a ≡ b) (b < a )
-              uz01 with pchainx⊆chain ia
-              ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib)))  ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib) 
-              ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u uz02 uz03 uz04 ⟫ (pchainx⊆chain ib) where
-                 a<b : IChain-i (proj2 ia) o< IChain-i (proj2 ib)
-                 a<b = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib
-                 uz02 : u o< osuc (IChain-i (proj2 ib))
-                 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b))
-                 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u
-                 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u
-                 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
-                 uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc
-          ... | tri≈ ¬a ia=ib ¬c = ? where
-              uz01 : Tri (* (& a ) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a ))
-              uz01 with proj2 ia | proj2 ib
-              ... | ic-init fca | ic-init fcb = fcn-cmp y f mf fca fcb
-              ... | ic-isup ia ia<x sa<x fca | ic-init fcb = ?
-              ... | ic-init fca | ic-isup ib ib<x sb<x fcb  = ?
-              ... | ic-isup ia ia<x sa<x fca | ic-isup ib ib<x sb<x fcb = fcn-cmp ? f mf ? ? 
-          ... | tri> ¬a ¬b ib<ia = uz01 where
-              uz01 : Tri (a < b) (a ≡ b) (b < a )
-              uz01 with pchainx⊆chain ib
-              ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia)  ⟪ bi , ch-init fc ⟫ 
-              ... | ⟪ bi , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-is-sup u uz02 uz03 uz04 ⟫  where
-                 b<a : IChain-i (proj2 ib) o< IChain-i (proj2 ia)
-                 b<a = ichain-inject {_} {_} {proj2 ib} {proj2 ia} ib<ia
-                 uz02 : u o< osuc (IChain-i (proj2 ia))
-                 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc b<a))
-                 uz03 : ZChain.supf (pzc (pic<x (proj2 ia))) u ≡ u
-                 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) )) su=u
-                 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ia))) u) (& b)
-                 uz04 = subst (λ k → FClosure A f k (& b)) ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) ) fc
+          ptotalx {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
+          ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainx⊆chain ib) 
+          ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainx⊆chain ib) 
+          ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
 
           usup : MinSUP A pchainx
           usup = minsupP pchainx (λ ic → ? ) ptotalx