# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668611092 -32400
# Node ID 9672214d4e13873247a0ca44c5a2fe3c95914c96
# Parent  ce713b5db3f3e432d57b6e7471714fdf2c6c0b6b
...

diff -r ce713b5db3f3 -r 9672214d4e13 src/zorn.agda
--- a/src/zorn.agda	Wed Nov 16 14:11:28 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 00:04:52 2022 +0900
@@ -83,6 +83,10 @@
 ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq))  y<z
 ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z
 
+ftrans<-<= : {x y z : Ordinal } →  x <<  y →  y <= z →  x <<  z
+ftrans<-<= {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y
+ftrans<-<= {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt 
+
 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y
 <=to≤ (case1 eq) = case1 (cong (*) eq)
 <=to≤ (case2 lt) = case2 lt
@@ -277,11 +281,24 @@
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 --
---         f (f ( ... (sup y))) f (f ( ... (sup z1)))
+--         f (f ( ... (supf y))) f (f ( ... (supf z1)))
 --        /          |         /             |
 --       /           |        /              |
---    sup y   <       sup z1          <    sup z2
+--    supf y   <       supf z1          <    supf z2
 --           o<                      o<
+--
+--    if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1
+
+
+fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal } 
+    → (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a
+fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl ))
+... | case1 eq = trans eq (sym a=b)
+... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-<= lt (≤to<= fc00 )) ) where
+     fc00 :  * b ≤ * (f b)
+     fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
+
+--
 -- data UChain is total
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
@@ -410,7 +427,7 @@
       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
       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
@@ -719,6 +736,8 @@
                   m06 : ChainP A f mf ay supf b
                   m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
                ... | case1 sb=sx = ? where
+                  b<A : b o< & A
+                  b<A = z09 ab
                   m09 : IsSUP A (UnionCF A f mf ay (ZChain.supf zc) b) ab
                   m09 = proj2 is-sup
                   m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
@@ -726,9 +745,26 @@
                         chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                   m05 : ZChain.supf zc b ≡ b
                   m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
-
                   m07 : MinSUP A (UnionCF A f mf ay supf (supf x)) -- supf z o< supf ( supf x )
                   m07 = ZChain.minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
+                  m29 : x o≤ & A
+                  m29 = ?
+                  m15 : supf (supf x) ≡ MinSUP.sup m07 
+                  m15 = ZChain.supf-is-minsup zc (o<→≤ (z09 (ZChain.asupf zc)))
+                  m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
+                  m17 = ZChain.minsup zc m29
+                  m18 : supf x ≡ MinSUP.sup m17 
+                  m18 = ZChain.supf-is-minsup zc m29
+                  m10 : f (supf b) ≡ supf b
+                  m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
+                      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 m29  fc
+                          m12 :  odef (UnionCF A f mf ay supf (& A)) z
+                          m12 = ZChain.fcs<sup zc ? ?  fc
+                          -- m14 :  odef (UnionCF A f mf ay supf x) z
+                          -- m14 = ZChain.fcs<sup zc ? ?
                   m08 : MinSUP A (UnionCF A f mf ay supf b)
                   m08 = ZChain.minsup zc (o<→≤ (z09 ab))           -- supf z o< supf b
 
@@ -741,11 +777,10 @@
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
                ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-               ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+               ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
+               ... | case2 sb<sx = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
                   m09 : b o< & A
                   m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                  sb<sx : supf b o< supf x
-                  sb<sx  = ?
                   m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
                   m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
                   m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
@@ -759,6 +794,17 @@
                   m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
                   m06 : ChainP A f mf ay supf b
                   m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
+               ... | case1 sb=sx = ? where
+                  m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
+                  m17 = ZChain.minsup zc ?
+                  m18 : supf x ≡ MinSUP.sup m17 
+                  m18 = ZChain.supf-is-minsup zc ?
+                  m10 : f (supf b) ≡ supf b
+                  m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
+                      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 ?  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 =