# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667826114 -32400
# Node ID 9bfe54cd9fb92157377f954dc47beede6fbf7afc
# Parent  2a67cae517d8fb0cf006e58a98daaf5a6cb8d01e
csupf removal?

diff -r 2a67cae517d8 -r 9bfe54cd9fb9 src/zorn.agda
--- a/src/zorn.agda	Mon Nov 07 17:56:03 2022 +0900
+++ b/src/zorn.agda	Mon Nov 07 22:01:54 2022 +0900
@@ -1173,6 +1173,21 @@
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m ? ?
 
+                 csupf10 : {z1 : Ordinal } → supf1 z1 o< supf1 x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
+                 csupf10 {z1} sz<sx = ⟪ asupf1 , ch-is-sup z1 sz<sx cs01 (init asupf1 refl ) ⟫ where
+                     cs01 : ChainP A f mf ay supf1 z1
+                     cs01 = record { fcy<sup = fcy<sup ; order = ? ; supu=u = ? } where
+                         fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 z1) ∨ (z << supf1 z1) 
+                         fcy<sup {z} fc with trio< z1 px
+                         ... | tri< a ¬b ¬c = ZChain.fcy<sup zc (o<→≤ a)  fc
+                         ... | tri≈ ¬a b ¬c = ZChain.fcy<sup zc (o≤-refl0 b) fc
+                         ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 (case1 ⟪ A∋fc _ fc , ch-init fc ⟫)
+                         order    : {s w : Ordinal} → (lt : supf1 s o< supf1 z1) → FClosure A f (supf1 s ) w → (w ≡ supf1 z1 ) ∨ ( w << supf1 z1 )
+                         order {s} {z1} lt fc with trio< z1 px
+                         ... | tri< a ¬b ¬c = ?
+                         ... | tri≈ ¬a b ¬c = ?
+                         ... | tri> ¬a ¬b c = MinSUP.x≤sup sup1 ?
+
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
                  csupf1 {z1} sz1<x = csupf2 where
                      --  z1 o< px → supf1 z1 ≡ supf0 z1