# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665553553 -32400
# Node ID d5293a7c2ec4da860f49e759b51229724d9a268f
# Parent  870a6b57dd39aa904098a4c1cbf0d11b102fb396
...

diff -r 870a6b57dd39 -r d5293a7c2ec4 src/zorn.agda
--- a/src/zorn.agda	Wed Oct 12 14:03:38 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 14:45:53 2022 +0900
@@ -1119,10 +1119,13 @@
 
                  csupfp : {w z : Ordinal } → supf1 w o< z → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 w) 
                  csupfp {w} {z} sw1<z z≤x with osuc-≡< z≤x
-                 ... | case1 eq = ?
-                 ... | case2 lt = ?  where
+                 ... | case1 refl = csupf1 sw1<z
+                 ... | case2 lt with trio< (supf0 w) z
+                 ... | tri< sw<z ¬b ¬c = ? where
                      csupfpx : odef (UnionCF A f mf ay supf0 z) (supf0 w) 
-                     csupfpx = ZChain.csupf zc ? ?
+                     csupfpx = ZChain.csupf zc sw<z (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) lt )
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b c =  ?
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)