# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666606279 -32400
# Node ID 3a511519bd1056b2716cef4d9a0e97bd099aae8d
# Parent  f160556a7c9af45f337021fe45844ced27c7437e
...

diff -r f160556a7c9a -r 3a511519bd10 src/zorn.agda
--- a/src/zorn.agda	Mon Oct 24 16:16:15 2022 +0900
+++ b/src/zorn.agda	Mon Oct 24 19:11:19 2022 +0900
@@ -1415,6 +1415,7 @@
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc 
                (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc  )  ss<sa ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
+
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)
           msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
@@ -1438,9 +1439,7 @@
           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)
-          -- z26 : {x : Ordinal } → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) x
-          --     → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) c) x ∨ odef (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ) x 
-          -- z26 = ?
+
           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)
@@ -1451,19 +1450,17 @@
                z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ?
                     -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
                     --     supf u o< spuf c → order
+
           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) ) ))
-               -- z26 : {x : Ordinal } → odef (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ) x → (x ≡ d ) ∨ (x << d )  
-               -- z26 lt with MinSUP.x<sup spd (subst (λ k → odef _ k ) ? lt)
-               -- ... | case1 eq = ?
-               -- ... | case2 lt = ?
-               -- z25 : {x : Ordinal } → odef (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y )  
-               -- z25 {x} (init au eq ) = ?   -- sup c = x, cf y ≡ d, sup c =< d
-               -- z25  (fsuc x lt) = ?        -- cf (sup c) 
+               z25 : odef (ZChain.chain zc) (cf nmx d)
+               z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
+                   (ZChain.f-next zc 
+                   (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp ))))
 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
@@ -1475,10 +1472,16 @@
                 d1 = MinSUP.sup spd
                 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
                 z24 = MinSUP.x<sup spd (init asc refl)
+                z26 :  odef (ZChain.chain zc) (supf mc)
+                z26 = ?
+                z28 : supf mc o< & A
+                z28 = z09 (ZChain.asupf zc)
                 z25 : supf mc << d1
                 z25 with z24
                 ... | case2 lt = lt
-                ... | case1 eq = ?
+                ... | case1 eq = ? where
+                    z27 :  odef (ZChain.chain zc) (cf nmx d1)
+                    z27 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k ) eq (ZChain.csupf zc z28))
 
           sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
           sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )