# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670035727 -32400
# Node ID 4b525726f2df264429b6122e4e54bc6eecc0451c
# Parent  4b22a2ece4e806f51d0a778aed41c2cb58401685
...

diff -r 4b22a2ece4e8 -r 4b525726f2df src/zorn.agda
--- a/src/zorn.agda	Sat Dec 03 09:57:13 2022 +0900
+++ b/src/zorn.agda	Sat Dec 03 11:48:47 2022 +0900
@@ -353,7 +353,9 @@
    chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
 
    mf : ≤-monotonic-f A f 
-   mf x ax = ? 
+   mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
+      mf00 : * x < * (f x)
+      mf00 = proj1 ( mf< x ax )
 
    f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a)
    f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫ 
@@ -714,7 +716,7 @@
                           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<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
+                  m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
@@ -730,7 +732,7 @@
                           m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                                 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 ⟫
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
@@ -928,6 +930,21 @@
                  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
 
+                 sfpx<x : supf0 px o< x
+                 sfpx<x with trio< (supf0 px) x
+                 ... | tri< a ¬b ¬c = a 
+                 ... | 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-≡< m13
+                      ... | case1 eq = eq
+                      ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) 
+                      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 m13 sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
+
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
                  cfcs : {a b w : Ordinal } 
@@ -1003,8 +1020,7 @@
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
                       csupf1 : odef (UnionCF A f ay supf1 b) w
-                      csupf1 with trio< (supf0 px) x
-                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫  where
+                      csupf1 = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫  where
                           spx = supf0 px
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
@@ -1012,17 +1028,6 @@
                           z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ sfpx<x ) )
                           fc1 : FClosure A f (supf1 spx) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
-                      ... | 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-≡< m13
-                          ... | case1 eq = eq
-                          ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) 
-                          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 m13 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 ay supf1 x) z → odef pchainpx z
@@ -1062,13 +1067,15 @@
                         → supf1 z o≤ s
                     z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where
                         z25 : {w : Ordinal } → odef pchainpx w → w ≤ s 
-                        z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) ? ?  ? ⟫ where
-                            z27 : supf1 px ≡ px    --- sp1 o≤ x
-                            z27 = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc ? ? ? )
-                            z29 : supf0 px o≤ z
-                            z29 = ? --    supf0 px ≡ supf1 px o≤ supf1 x o≤ 
-                            z28 : supf0 px o< z
-                            z28 = ?
+                        z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where
+                            z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x o≤ 
+                            z28 = subst (λ k → supf0 px o< k) (sym z=x) sfpx<x
+                            z29 : supf0 px o≤ px 
+                            z29 = zc-b<x _ sfpx<x
+                            z27 : supf1 (supf0 px) ≡ supf0 px
+                            z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 )
+                            fc1 : FClosure A f (supf1 (supf0 px)) w
+                            fc1 = subst (λ k → FClosure A f k w) (sym z27) fc
                         z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
                         z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc  ⟫) = sup ⟪ ua , ch-is-sup u u<z
                              (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where