# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669334248 -32400
# Node ID eee019e64beaff57772d1c8760f7fe5497b7788d
# Parent  eb2d0fb19b67623dc61df2e19af9aa03947b0d74
...

diff -r eb2d0fb19b67 -r eee019e64bea src/zorn.agda
--- a/src/zorn.agda	Thu Nov 24 12:30:41 2022 +0900
+++ b/src/zorn.agda	Fri Nov 25 08:57:28 2022 +0900
@@ -1120,8 +1120,14 @@
                       --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
                       z50 : odef (UnionCF A f mf ay supf1 b) w
                       z50 with osuc-≡< px≤sa
-                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) ? ? (subst (λ k → FClosure A f k w) ? fc)  ⟫ 
-                      ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) ? ⟫  ) 
+                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 ? (subst (λ k → FClosure A f k w) z52 fc)  ⟫ where
+                          z51 : supf0 px o< b
+                          z51 = ?
+                          z52 : supf1 a ≡ supf1 (supf0 px)
+                          z52 = ?
+                      ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫  ) where
+                          z53  : supf1 a o< x
+                          z53  = ordtrans<-≤ sa<b b≤x
                  ... | case1 sa<px with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
                       z50 : odef (UnionCF A f mf ay supf1 b) w
@@ -1182,10 +1188,8 @@
                                    (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
                                    (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
                                        spx≤px ss0<spx (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
-                                          ss0<spx : supf0 s o< spx 
-                                          ss0<spx = ?
-                                          ss<px : supf0 s o< px
-                                          ss<px = osucprev ( begin
+                                          ss0<spx : supf0 s o< spx
+                                          ss0<spx = osucprev ( begin
                                             osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 ( begin
                                                s <⟨ supf-inject0 supf1-mono ss<spx ⟩
                                                supf0 px  ≤⟨ spx≤px ⟩
@@ -1193,8 +1197,7 @@
                                             osuc (supf1 s)  ≤⟨ osucc ss<spx ⟩
                                             supf1 spx  ≡⟨ sf1=sf0 spx≤px  ⟩
                                             supf0 spx  ≤⟨ ZChain.supf-mono zc spx≤px ⟩
-                                            supf0 px  ≤⟨ spx≤px ⟩
-                                            px ∎  ) where open o≤-Reasoning O
+                                            supf0 px  ∎  ) where open o≤-Reasoning O
                           cp1 : ChainP A f mf ay supf1 spx
                           cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) 
                                   ( ZChain.fcy<sup zc spx≤px fc )
@@ -1283,12 +1286,24 @@
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                      → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
-                 ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) ? fc
-                 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl ? fc
-                 ... | tri> ¬a ¬b px<b with trio< a px
-                 ... | tri< a ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) ( ZChain.cfcs zc mf< a o≤-refl ? fc )
-                 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c )
-                 ... | tri≈ ¬a refl ¬c = ? --  supf0 px o< x  → odef (UnionCF A f mf ay supf0 x) (supf0 px)
+                 ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc
+                 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc 
+                 ... | tri> ¬a ¬b px<b = ? where
+                     x=b : x ≡ b
+                     x=b = ?
+                     --  a o< x, supf a o< x
+                     --      a o< px , supf a o< px → odef U w
+                     --      a ≡ px         -- supf0 px o< x → odef U w
+                     --                     -- x o≤ supf0 px o< x → ⊥
+                     --      supf a ≡ px    -- a o< px → odef U w
+                     --                        a ≡ px → supf px ≡ px → odef U w
+
+                     cfcs1 : odef (UnionCF A f mf ay supf0 b) w
+                     cfcs1 with trio< a px
+                     ... | tri< a<px ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
+                             ( ZChain.cfcs zc mf< a<px o≤-refl ? fc ) 
+                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c )
+                     ... | tri≈ ¬a refl ¬c = ? --  supf0 px o< x  → odef (UnionCF A f mf ay supf0 x) (supf0 px)
                                            --  x o≤ supf0 px o≤ sp  →
 
                  zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
@@ -1441,10 +1456,10 @@
           ... | case1 b=x with trio< a x 
           ... | tri< a<x ¬b ¬c = zc40 where
                sa = ZChain.supf (pzc  (ob<x lim a<x)) a
-               m =  omax a sa
+               m =  omax a sa     -- x is limit ordinal, so we have sa o< m o< x
                m<x : m o< x
                m<x with trio< a sa | inspect (omax a) sa
-               ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim ?
+               ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim (ordtrans<-≤ sa<b b≤x )
                ... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
                    zc41 : omax a sa o< x
                    zc41 = osucprev ( begin
@@ -1468,7 +1483,7 @@
                ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫  where -- u o< px → u o< b ?
                    zc55 : u o< osuc m
                    zc55 = u<x
-                   u<b : u o< b --      b o≤ u → b o≤ a -- u ≡ supf1 a
+                   u<b : u o< b 
                    u<b = subst (λ k → u o< k ) (sym b=x) ( ordtrans u<x (ob<x lim m<x))
                    fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
                    fc1m = fc1
@@ -1482,15 +1497,19 @@
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
                supfb =  ZChain.supf (pzc (ob<x lim b<x)) 
+               sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a 
+               sb=sa {a} a<b = trans (sf1=sf (ordtrans<-≤ a<b b≤x)) (zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ <-osuc) )
                fcb : FClosure A f (supfb a) w
-               fcb = ?
-               --  supfb a o≤ supfb b
+               fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc 
+               --  supfb a o< b assures it is in Union b
                zcb : odef (UnionCF A f mf ay supfb b) w
-               zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) ? fcb
+               zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
                zc40 : odef (UnionCF A f mf ay supf1 b) w
                zc40 with zcb
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x ? ? ⟫  
+               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x cp (subst (λ k → FClosure A f k w) (sym (sb=sa u<x)) fc1 ) ⟫ where
+                   cp : ChainP A f mf ay supf1 u
+                   cp = ?
                  
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function