# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669976081 -32400
# Node ID 23e185ef27378cb6c7cf1f2f822e4ba72afaefb1
# Parent  23a8e4d558e048b057a99830b7fb240832c6b2e2
...

diff -r 23a8e4d558e0 -r 23e185ef2737 src/zorn.agda
--- a/src/zorn.agda	Fri Dec 02 15:49:50 2022 +0900
+++ b/src/zorn.agda	Fri Dec 02 19:14:41 2022 +0900
@@ -1057,9 +1057,13 @@
                         → supf1 z o≤ s
                     z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where
                         z25 : {w : Ordinal } → odef pchainpx w → w ≤ s 
-                        z25 {w} (case2 fc) = sup ⟪ ? , ch-is-sup px px<z z27 (fcpu fc ?) ⟫ where
+                        z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) ? ?  ? ⟫ where
                             z27 : supf1 px ≡ px    --- sp1 o≤ x
-                            z27 = ?
+                            z27 = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc ? ? ? )
+                            z29 : supf0 px o≤ z
+                            z29 = ? --    supf0 px ≡ supf1 px o≤ supf1 x o≤ x ≡ z
+                            z28 : supf0 px o< z
+                            z28 = ?
                         z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
                         z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc  ⟫) = sup ⟪ ua , ch-is-sup u u<z
                              (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where