# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668623599 -32400
# Node ID a15f1cddf4c6822ff8e9ad18cb76c935b9c2e1f2
# Parent  e11c244d7eacf7ca1caacc9c26383634df6d4e61
u ≤ x again?

diff -r e11c244d7eac -r a15f1cddf4c6 src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 02:33:06 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 03:33:19 2022 +0900
@@ -431,6 +431,7 @@
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
            → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b
       fcs<sup : {a b w : Ordinal } → a o< b → b o≤ z → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
+
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
@@ -438,7 +439,15 @@
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x)
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
-      csupf : {b : Ordinal } → supf b o< supf z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+
+   -- fcs<sup implirs supf-mono and supf-<
+   -- ¬ ( HasPreb A A f (supf b)
+   -- supf-mono' : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
+   -- supf-mono' {x} {y} x≤y with osuc-≡< x≤y
+   -- ... | case1 eq = o≤-refl0 ( cong supf eq )
+   -- ... | case2 lt with fcs<sup lt ? (init asupf refl)
+   -- ... | ⟪ ua , ch-init fc ⟫ = ?
+   -- ... | ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?
 
    chain : HOD
    chain = UnionCF A f mf ay supf z
@@ -482,6 +491,9 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
+   csupf : {b : Ordinal } → supf b o< supf z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+   csupf {b} sb<sz = fcs<sup (supf-inject sb<sz) o≤-refl (init asupf refl)
+
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
    fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
@@ -950,7 +962,7 @@
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; fcs<sup = ?  }  where
                  --  supf0 px is included in the chain of sp1
                  --  supf0 px ≡ px ∧ supf0 px o< sp1 → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
                  --     else                             UnionCF A f mf ay supf0 px  ≡ UnionCF supf1 x
@@ -1019,6 +1031,12 @@
                  fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z
                  fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
 
+                 fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 fcs<sup with trio< a px
+                 ... | tri< a ¬b ¬c = ? -- chain-mono ZChain.fcs<sup a
+                 ... | tri≈ ¬a b ¬c = ? -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 
+                 ... | tri> ¬a ¬b c = ? --  px o< a o< b o≤ x
+
                  zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
                  zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
                  zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
@@ -1081,25 +1099,9 @@
                         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 ? ?
 
-                 csupf0 : {z1 : Ordinal } → supf1 z1 o< supf1 px → z1 o≤ px  → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                 csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) (
-                       UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ 
-                         (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) 
-                         (ZChain.csupf zc ? ))) -- (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
-                 -- px o< z1 , px o≤ supf1 z1  -->   px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1
-
-                 csupf1 : {z1 : Ordinal } → supf1 z1 o< supf1 x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                 csupf1 {z1} sz<sx = ⟪ asupf1 , ch-is-sup (supf1 z1) (subst (λ k → k o< supf1 x) (sym cs00) sz<sx) cp (init asupf1 cs00 ) ⟫ where
-                     z<x : z1 o< x
-                     z<x = supf-inject0 supf1-mono sz<sx
-                     cs00 :  supf1 (supf1 z1) ≡ supf1 z1
-                     cs00 = ?
-                     cp : ChainP A f mf ay supf1 (supf1 z1) 
-                     cp = ?
-
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; fcs<sup = ?    }  where
 
                  --  supf0 px not is included by the chain
                  --     supf1 x ≡ supf0 px because of supfmax