# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662978932 -32400
# Node ID 166bee3ddf4c79fb048e8f009ca96d1b8b6dab88
# Parent  8a49ab1dcbd0481274215b06279a1c008fa7a46e
...

diff -r 8a49ab1dcbd0 -r 166bee3ddf4c src/zorn.agda
--- a/src/zorn.agda	Sun Sep 11 19:58:49 2022 +0900
+++ b/src/zorn.agda	Mon Sep 12 19:35:32 2022 +0900
@@ -369,6 +369,34 @@
       supf-is-sup : {x : Ordinal } → supf x ≡ & (SUP.sup (sup x) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 
+--
+--         f (f ( ... (sup y))) f (f ( ... (sup z1)))
+--        /          |         /             |
+--       /           |        /              |
+--    sup y   <       sup z1          <    sup z2
+--           o<                      o<
+
+smono→SUPU : (A : HOD) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)  
+   → {x z : Ordinal } → { supf : Ordinal → Ordinal } 
+   → ( supf x ≡ z ) → ( {x y : Ordinal } → x o≤  y → supf x o≤ supf y )
+                      → ( {x y : Ordinal } → x o≤  y → supf x <= supf y )
+   → (sz : SUP A (UnionCF A f mf ay (λ _ → z) x)) → (su : SUP A (UnionCF A f mf ay supf x)) → & (SUP.sup sz) ≡ & (SUP.sup su)
+smono→SUPU A f mf {y} ay {x} {z} {supf} sx=z mono mono< s = ? where
+      sup = SUP.sup s
+      x<sup : {w : HOD} → (UnionCF A f mf ay supf x) ∋ w → (w ≡ sup ) ∨ (w < sup )   
+      x<sup {w} ⟪ au , ch-init fc ⟫ = SUP.x<sup s ⟪ au , ch-init fc ⟫ 
+      x<sup {w} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ with trio< u z
+      ... | tri< a ¬b ¬c = ?  where
+            zc01 :  {s : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) (& w) → ((& w) ≡ supf u ) ∨ ( (& w)  << supf u )
+            zc01 = ChainP.order is-sup 
+      ... | tri≈ ¬a b ¬c = ?
+      ... | tri> ¬a ¬b z<u = ⊥-elim ( o≤> u≤z z<u ) where
+            u≤z :  u o≤ z
+            u≤z = begin u ≡⟨ sym (ChainP.supu=u is-sup)  ⟩ 
+                  supf u  ≤⟨ mono (o<→≤ u<x  )  ⟩ 
+                  supf x  ≡⟨ sx=z ⟩ 
+                  z  ∎ where open  o≤-Reasoning O 
+
 
 zsupf : (A : HOD) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) 
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
@@ -377,20 +405,32 @@
 
     zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZSupf A f mf ay y₁) → ZSupf A f mf ay x
     zc1 x prev with Oprev-p x
-    ... | yes op = record { supf = ? ; sup = ? ; spuf-is-sup = ? ; supf-mono = ? }  where
+    ... | yes op = record { supf = ? ; sup = ? ; supf-is-sup = ? ; supf-mono = ? }  where
        px = Oprev.oprev op
+       pchain : HOD
+       pchain = UnionCF A f mf ay (ZSupf.supf ( prev px (pxo<x op) )) px
        zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
        zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+
        supf : Ordinal → Ordinal
        supf z with trio< z px
-       ... | tri< a ¬b ¬c = ZSupf.spuf (prev (ordtrans a (pxo<x op))) z
-       ... | tri≈ ¬a b ¬c = ZSupf.spuf (prev (subst (λ k → k o< x ) b (pxo<x op))) z
-       ... | tri> ¬a ¬b px<x with ODC.∋-p O A (* x)
-       ... | no noax = ZSupf.spuf (prev o≤-refl ) px
-       ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) z f )   
-       ... | case1 pr = ZSupf.spuf (prev o≤-refl ) px
-       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
-       ... | case2 ¬x=sup = ZSupf.spuf (prev o≤-refl ) px
+       ... | tri< a ¬b ¬c = ZSupf.supf (prev z (ordtrans a (pxo<x op))) z
+       ... | tri≈ ¬a b ¬c = ZSupf.supf (prev z (subst (λ k → k o< x ) (sym b) (pxo<x op))) z
+       ... | tri> ¬a ¬b px<x = ZSupf.supf (prev px (pxo<x op) ) px
+
+       supf1 : Ordinal → Ordinal
+       supf1 z with trio< z px
+       ... | tri< a ¬b ¬c = ZSupf.supf (prev z (ordtrans a (pxo<x op))) z
+       ... | tri≈ ¬a b ¬c = ZSupf.supf (prev z (subst (λ k → k o< x ) (sym b) (pxo<x op))) z
+       ... | tri> ¬a ¬b px<x = & (SUP.sup (zsupf0 A f mf ay supP ax))
+
+       zc2 : ZSupf A f mf ay x
+       zc2 with ODC.∋-p O A (* x)
+       ... | no noax = ?
+       ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain z f )   
+       ... | case1 pr = ?
+       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
+       ... | case2 ¬x=sup = ?
        ... | case1 is-sup = ?
 
     ... | no lim = ?  where
@@ -402,15 +442,15 @@
        supfx :  Ordinal
        supfx with ODC.∋-p O A (* x)
        ... | no noax = supfmax
-       ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) z f )   
+       ... | yes ax with ODC.p∨¬p O ( HasPrev A ? x f )   
        ... | case1 pr = supfmax
-       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
+       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A ? ax )
        ... | case2 ¬x=sup = supfmax
        ... | case1 is-sup = ?
 
        supf : Ordinal → Ordinal
        supf z with trio< z x
-       ... | tri< a ¬b ¬c = ZSupf.spuf a z
+       ... | tri< a ¬b ¬c = ZSupf.supf (prev z a) z
        ... | tri≈ ¬a b ¬c = supfx
        ... | tri> ¬a ¬b px<x = supfx