# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668749660 -32400
# Node ID 71f231c9ed6ff0a029484d95a892e12199a81061
# Parent  3ffbdd53d1ea1b6e5d602d6debde986fe1cca35e
...

diff -r 3ffbdd53d1ea -r 71f231c9ed6f src/zorn.agda
--- a/src/zorn.agda	Fri Nov 18 09:41:13 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 14:34:20 2022 +0900
@@ -430,7 +430,8 @@
       supf :  Ordinal → Ordinal
       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
+      fcs<sup : (mf< : <-monotonic-f A f)
+         {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
@@ -491,8 +492,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)
+   csupf : (mf< : <-monotonic-f A f) {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 mf< {b} sb<sz = fcs<sup mf< (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)
@@ -504,11 +506,11 @@
 
    IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
        → ({y : Ordinal} → odef (UnionCF A f mf ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
-       → ( {a : Ordinal } → a << f a )
+       → ( {a : Ordinal } → odef A a → a << f a )
        → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f sp )
    IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr ( <=to≤  fsp≤sp) sp<fsp ) where
        sp<fsp : sp << f sp
-       sp<fsp = <-mono-f
+       sp<fsp = <-mono-f asp
        pr = HasPrev.y hp
        im00 : f (f pr) <= sp
        im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
@@ -696,7 +698,7 @@
                 s<z : s o< & A
                 s<z = ordtrans s<b b<z
                 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z)))
+                zc04 = ZChain.csupf zc mf< (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z)))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
@@ -758,7 +760,7 @@
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.fcs<sup zc b<x x≤A  fc
+                          m13 = ZChain.fcs<sup zc mf< b<x x≤A  fc
 
         ... | no lim = record { is-max = is-max ; order = order }  where
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
@@ -796,7 +798,7 @@
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.fcs<sup zc b<x x≤A  fc
+                          m13 = ZChain.fcs<sup zc mf< b<x x≤A  fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -1031,12 +1033,13 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 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 {a} {b} {w} a<b b≤x fc with trio< a px
+                 fcs<sup : (mf< : <-monotonic-f A f) {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 mf< {a} {b} {w} a<b b≤x fc with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
                       z50 : odef (UnionCF A f mf ay supf1 b) w
                       z50 with osuc-≡< b≤x
-                      ... | case2 lt with ZChain.fcs<sup zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) fc  
+                      ... | case2 lt with ZChain.fcs<sup zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                       ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px )  ⟫  where -- u o< px → u o< b ?
                            u≤px : u o≤ px
@@ -1050,7 +1053,7 @@
                                    (sym (sf=eq u<x)) s<u)  
                                     (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
                                ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
-                      z50 | case1 eq with ZChain.fcs<sup zc a<px o≤-refl fc  
+                      z50 | case1 eq with ZChain.fcs<sup zc mf< a<px o≤-refl fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                       ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
                            u<b : u o< b
@@ -1064,8 +1067,8 @@
                                    (sym (sf=eq u<x)) s<u)  
                                     (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
                                ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
-                 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b cp1 ? ⟫ where 
-                      -- a ≡ px , b ≡ x, sp o≤ x → supf px o< x 
+                 ... | tri≈ ¬a a=px ¬c = csupf1 where
+                      -- a ≡ px , b ≡ x, sp o≤ x 
                       px<b : px o< b
                       px<b = subst₂ (λ j k → j o< k) a=px refl a<b
                       b=x : b ≡ x
@@ -1075,20 +1078,35 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
                       z51 : FClosure A f (supf1 px) w
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
-                      -- what happens if supf0 px ≡ x ?    supf0 px ≡ sp ≡ x
-                      --     this does not happen in <-monotonic case
-                      csupf1 : odef (UnionCF A f mf ay supf1 x) (supf0 px)
-                      csupf1 = ⟪ ?  , ch-is-sup (supf0 px) z52 ? (init ? ? ) ⟫ where
-                          z52 : supf0 px o< x
-                          z52 = ?
-                      -- cspx : odef (UnionCF A f mf ay supf0 px) (supf0 px)
-                      -- cspx = ZChain.csupf zc ?
-                      spx=px : supf1 px ≡ px
-                      spx=px = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc (subst (λ k → odef A k) ? ?)  o≤-refl ? )
-                      cp1 : ChainP A f mf ay supf1 px
-                      cp1 = record { fcy<sup = λ {z} fc → ? 
-                               ; order =  λ {s} {z} s<u fc  → ? 
-                               ; supu=u = spx=px }
+                      csupf1 : odef (UnionCF A f mf ay supf1 b) w
+                      csupf1 with trio< (supf0 px) x
+                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup (supf0 px) (subst (λ k → supf0 px o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫  where 
+                          -- supf0 px o< x ,   supf0 px is member of (UnionCF A f mf ay supf1 x)
+                          z53 : odef A w
+                          z53 = A∋fc {A} _ f mf fc
+                          z54 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
+                          z54 {z} ⟪ az , ch-init fc ⟫ = ?
+                          z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ?
+                          z52 : supf1 (supf0 px) ≡ supf0 px
+                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x) 
+                             ⟪ record { x≤sup = z54  } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ )
+                          fc1 : FClosure A f (supf1 (supf0 px)) w
+                          fc1 = subst (λ k → FClosure A f k w ) (trans ? (sym z52)) fc
+                          cp1 : ChainP A f mf ay supf1 (supf0 px)
+                          cp1 = record { fcy<sup = λ {z} fc → ? 
+                                   ; order =  λ {s} {z} s<u fc  → ? 
+                                   ; supu=u = z52 } 
+                      ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
+                          -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
+                          m12 : supf0 px ≡ sp1
+                          m12 with osuc-≡< sfpx≤sp1
+                          ... | case1 eq = eq
+                          ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) -- supf0 px o< sp1 , x o< sp1
+                          m10 : f (supf0 px) ≡ supf0 px
+                          m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where
+                              m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1)
+                              m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc)  
+                      ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans sfpx≤sp1 sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
 
                  zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z