# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666430776 -32400
# Node ID a6d97e6e5309266ac582da6c95365b98abfcb1c0
# Parent  330303f0c68867b6acafc94d5ac9054bc60baf98
...

diff -r 330303f0c688 -r a6d97e6e5309 src/zorn.agda
--- a/src/zorn.agda	Sat Oct 22 11:15:17 2022 +0900
+++ b/src/zorn.agda	Sat Oct 22 18:26:16 2022 +0900
@@ -1423,10 +1423,29 @@
           d = MinSUP.sup spd
           d<A : d o< & A
           d<A =  ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
+          msup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf d)
+          msup = ZChain.minsup zc (o<→≤ d<A) 
           sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
           sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
+          is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
+          is-sup = record { x<sup = z22 } where
+               -- 
+               z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
+               z23 lt = MinSUP.x<sup spd lt
+               z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
+                   (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
+               z22 {y} zy = ?
+               -- with MinSUP.x<sup spd ? -- (subst (λ k → odef _ k ) (sym &iso) zy)
+               -- ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )
+               -- ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
+          not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx)
+          not-hasprev hp = ? where
+               y : Ordinal
+               y = HasPrev.y hp
+               z24 : y << d
+               z24 = subst (λ k → y <<  k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
           sd=d : supf d ≡ d
-          sd=d = ?
+          sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
           sc<d : supf c << d
           sc<d = ? where
               z21 = proj1 ( cf-is-<-monotonic nmx ? ? )