# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669256326 -32400
# Node ID c63f1fadd27f47ddb62ae7fc94565ec80751ae5e
# Parent  ffdfd8d1303abd9d6eac147303f03abd6a5752f7
sa<b

diff -r ffdfd8d1303a -r c63f1fadd27f src/zorn.agda
--- a/src/zorn.agda	Thu Nov 24 10:49:29 2022 +0900
+++ b/src/zorn.agda	Thu Nov 24 11:18:46 2022 +0900
@@ -431,7 +431,7 @@
       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
       cfcs : (mf< : <-monotonic-f A f)
-         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< z  → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf z) w
+         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → 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
@@ -529,7 +529,7 @@
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
        z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) 
                    (sym (supf-is-minsup b≤z)) 
-                   (MinSUP.x≤sup (minsup b≤z) ?) where
+                   (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z ? fc )) where
                u<b : u o< b
                u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x )
                su<z : supf u o< z
@@ -859,7 +859,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.cfcs zc mf< b<x x≤A (ZChain.supf<A zc) fc
+                          m13 = ZChain.cfcs 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 →
@@ -897,7 +897,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.cfcs zc mf< b<x x≤A (ZChain.supf<A zc) fc
+                          m13 = ZChain.cfcs 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 =
@@ -1099,28 +1099,28 @@
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x → supf1 a o< x  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 x) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with zc43 (supf0 a) px
+                     → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
                  ... | case2 px≤sa = z50 where
                       a≤px : a o≤ px
                       a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
                       --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
                       --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-                      z50 : odef (UnionCF A f mf ay supf1 x) w
+                      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)) sa<x ⟫  ) 
+                      ... | 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 sa<px with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
-                      z50 : odef (UnionCF A f mf ay supf1 x) w
+                      z50 : odef (UnionCF A f mf ay supf1 b) w
                       z50 with osuc-≡< b≤x
-                      ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<px fc  
+                      ... | case2 lt with ZChain.cfcs 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 ? cp1 (fcpu fc u≤px )  ⟫  where -- u o< px → u o< b ?
+                      ... | ⟪ 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
-                           u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b ? )
+                           u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b b≤x )
                            u<x : u o< x
-                           u<x = ordtrans<-≤ u<b ? --b≤x 
+                           u<x = ordtrans<-≤ u<b b≤x 
                            cp1 : ChainP A f mf ay supf1 u
                            cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc )  
                                ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) 
@@ -1130,7 +1130,7 @@
                                ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
                       z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                      ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u ? cp1 (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
+                      ... | ⟪ 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
                            u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc )
                            u<x : u o< x
@@ -1155,9 +1155,9 @@
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
-                      csupf1 : odef (UnionCF A f mf ay supf1 x) w
+                      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 spx ? cp1 fc1 ⟫  where
+                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫  where
                           spx = supf0 px
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
@@ -1168,9 +1168,8 @@
                           order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
                           order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
                                    (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
-                                   (MinSUP.x≤sup (ZChain.minsup zc spx≤px) ? )  where
-                                    -- (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                    --    spx≤px ss<px (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
+                                   (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
+                                       spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
                                           ss<px : supf0 s o< px
                                           ss<px = osucprev ( begin
                                             osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 ( begin
@@ -1268,12 +1267,12 @@
                  --     supf1 x ≡ supf0 px because of supfmax
 
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x →  supf0 a o< x → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 x) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<x 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
+                     → 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 = 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)
                                            --  x o≤ supf0 px o≤ sp  →
@@ -1423,15 +1422,15 @@
           ... | tri> ¬a ¬b c = ?
 
           cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                 → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 x) w
-          cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with osuc-≡< b≤x
+                 → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+          cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
           ... | 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<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 sa<x
+               ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim ?
                ... | 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
@@ -1449,10 +1448,10 @@
                fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
                zcm : odef (UnionCF A f mf ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
                zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-               zc40 : odef (UnionCF A f mf ay supf1 x) w
+               zc40 : odef (UnionCF A f mf ay supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u ? ? fc2 ⟫  where -- u o< px → u o< b ?
+               ... | ⟪ 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
@@ -1467,17 +1466,16 @@
                        zc57 = osucc u<x
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
-          cfcs mf< {a} {b} {w} a<b b≤x sa<x fc | case2 b<x = zc40 where
+          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)) 
                fcb : FClosure A f (supfb a) w
                fcb = ?
                --  supfb a o≤ supfb b
-               --  supfb (supfb a) o≤ supfb b
                sa<b : supfb a o< osuc b
                sa<b = ?
-               zcb : odef (UnionCF A f mf ay supfb x) w
-               zcb = ? -- ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) sa<b fcb
-               zc40 : odef (UnionCF A f mf ay supf1 x) w
+               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
+               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 ? ? ⟫