# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667555744 -32400
# Node ID 811135ad19045bd20cd5163d6a301c0d8258e3e7
# Parent  b7370c39769e4ed8a851d650164e1a81103ca3fc
supf sp = sp ?

diff -r b7370c39769e -r 811135ad1904 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 04 17:27:12 2022 +0900
+++ b/src/zorn.agda	Fri Nov 04 18:55:44 2022 +0900
@@ -483,27 +483,6 @@
        fsp≤sp : f sp <=  sp
        fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
 
-   IsMinSUP< : ( {a : Ordinal } → a << f a )
-       → {b x : Ordinal } → {ab : odef A b}  → x o≤ z → b o< x 
-       → IsMinSUP A (UnionCF A f mf ay supf x) f ab → IsMinSUP A (UnionCF A f mf ay supf b) f ab
-   IsMinSUP< <-mono-f {b} {x} {ab} x≤z b<x record { x≤sup = x≤sup ; minsup = minsup ; not-hp = nhp } 
-     = record { x≤sup = m02 ; minsup = m07 ; not-hp = IsMinSUP→NotHasPrev ab m02 <-mono-f } where
-             m02 : {z : Ordinal} → odef (UnionCF A f mf ay supf b) z → (z ≡ b) ∨ (z << b)
-             m02 {z} uz = x≤sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz) 
-             m10 : {s : Ordinal }  →  (odef A s ) 
-                →  ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) ) 
-                →    {w : Ordinal} → odef (UnionCF A f mf ay supf x) w → (w ≡ s) ∨ (w << s)
-             m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ?
-             m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where
-                m01 : w <= s
-                m01 with trio< (supf u) (supf b)
-                ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ 
-                ... | tri≈ ¬a b ¬c = ?
-                ... | tri> ¬a ¬b c = ?
-             m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
-                odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-             m07 {s} as b-is-sup = minsup as (m10 as b-is-sup )
-
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
@@ -1399,16 +1378,31 @@
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp
-                (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
-               ... | case2 lt = lt -- subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
+               ... | case2 lt = lt 
                z19 : IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp
-               z19 = record {   x≤sup = z20 ; minsup = ?  ; not-hp = ZChain.IsMinSUP→NotHasPrev zc ? z20 ? }  where
+               z19 = record {   x≤sup = z20 ; minsup = z21  ; not-hp = ZChain.IsMinSUP→NotHasPrev zc ? z20 ? }  where
+                   z23 : {z : Ordinal } → odef chain z → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z 
+                   z23 {z} ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                   z23 {z} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ = ⟪ au , ch-is-sup u z24 is-sup fc ⟫ where
+                       z26 : supf sp <= sp
+                       z26 = MinSUP.x≤sup sp1 ⟪ ?
+                           , ch-is-sup sp ? ? (init (ZChain.asupf zc) ? )  ⟫ 
+                       z25 : u <= sp
+                       z25 = MinSUP.x≤sup sp1 ⟪ subst (λ k → odef A k) (ChainP.supu=u is-sup) (ZChain.asupf zc) 
+                           , ch-is-sup u u<x is-sup (init (ZChain.asupf zc) (ChainP.supu=u is-sup))  ⟫ 
+                       z24 : supf u o< supf sp
+                       z24 = ? -- with ZChain.supf-<= zc z25
+                   z21 : {sup1 : Ordinal} → odef A sup1 
+                       → ({z : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z → (z ≡ sup1) ∨ (z << sup1)) 
+                       → sp o≤ sup1
+                   z21 {s} as s-sup = MinSUP.minsup sp1 as ( λ uz → s-sup (z23 uz) )
                    z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
-                   z20 {y} zy with MinSUP.x≤sup sp1 (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
+                   z20 {y} zy with MinSUP.x≤sup sp1 
+                       (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p ) 
                    ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p )
            z14 :  f sp ≡ sp