# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669387144 -32400
# Node ID e4919cc0cfe898fe08c851ae9cbf0fbf7d3bb1d8
# Parent  ab72526316bd3b9911f8faec937e8485f0ccae46
...

diff -r ab72526316bd -r e4919cc0cfe8 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 25 18:21:08 2022 +0900
+++ b/src/zorn.agda	Fri Nov 25 23:39:04 2022 +0900
@@ -987,7 +987,7 @@
 
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x sp1
-          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
+          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono 
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?  }  where
 
                  supf1 : Ordinal → Ordinal
@@ -1067,21 +1067,62 @@
                       --       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) z51 ? (subst (λ k → FClosure A f k w) z52 fc)  ⟫ where
+                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc)  ⟫ where
                           sa≤px : supf0 a o≤ px
                           sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
                           z51 : supf0 px o< b
                           z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ 
-                             supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ 
-                             supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 
-                             supf1 a ∎ )) sa<b where open ≡-Reasoning
+                                supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ 
+                                supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 
+                                supf1 a ∎ )) sa<b where open ≡-Reasoning
                           z52 : supf1 a ≡ supf1 (supf0 px)
                           z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 
-                             supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
-                             supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
-                             supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ 
-                             supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa)  ⟩ 
-                             supf1 (supf0 px) ∎ where open ≡-Reasoning
+                                supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
+                                supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
+                                supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ 
+                                supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa)  ⟩ 
+                                supf1 (supf0 px) ∎ where open ≡-Reasoning
+                          m : MinSUP A (UnionCF A f mf ay supf0 px)
+                          m = ZChain.minsup zc o≤-refl
+                          m=spx : MinSUP.sup m ≡ supf1 (supf0 px)
+                          m=spx = begin 
+                                MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl)  ⟩ 
+                                supf0 px ≡⟨ cong supf0 px=sa  ⟩ 
+                                supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px  ⟩
+                                supf0 a ≡⟨ sym (sf1=sf0 a≤px)  ⟩ 
+                                supf1 a ≡⟨ z52  ⟩ 
+                                supf1 (supf0 px)  ∎  where open ≡-Reasoning 
+                          z53 : supf1 (supf0 px) ≡ supf0 px
+                          z53 = begin
+                                supf1 (supf0 px)  ≡⟨ sym z52 ⟩ 
+                                supf1 a  ≡⟨ sf1=sf0 a≤px ⟩ 
+                                supf0 a  ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
+                                supf0 (supf0 a)  ≡⟨ sym ( cong supf0 px=sa ) ⟩ 
+                                supf0 px  ∎  where open ≡-Reasoning 
+                          cp : ChainP A f mf ay supf1 (supf0 px)
+                          cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪  A∋fc _ f mf fc , ch-init fc ⟫ )  
+                            ; order = order 
+                            ; supu=u = z53 } where
+                             uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                             uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) 
+                                     (sf1=sf0 (o<→≤ s<px))  fc ) where
+                                s<px : s o< px
+                                s<px = ZChain.supf-inject zc (osucprev ( begin
+                                     osuc (supf0 s)  ≡⟨ sym (cong osuc (sf1=sf0 ?) )  ⟩  
+                                     osuc (supf1 s)  ≤⟨ osucc ss<sp  ⟩ 
+                                     supf1 (supf0 px)  ≡⟨ z53  ⟩ 
+                                     supf0 px ∎ ))   where open o≤-Reasoning O
+                                ss<px : supf0 s o< px
+                                ss<px = osucprev ( begin
+                                     osuc (supf0 s)  ≡⟨ sym (cong osuc (sf1=sf0 ?) )  ⟩ 
+                                     osuc (supf1 s)  ≤⟨ osucc ss<sp  ⟩ 
+                                     supf1 (supf0 px)  ≡⟨ sym z52  ⟩ 
+                                     supf1 a  ≡⟨ sf1=sf0 a≤px  ⟩ 
+                                     supf0 a  ≡⟨ sym px=sa  ⟩ 
+                                     px ∎ )   where open o≤-Reasoning O
+                             order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) →
+                                    FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px))
+                             order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m (uz s<u 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)) z53 ⟫  ) where
                           z53  : supf1 a o< x
                           z53  = ordtrans<-≤ sa<b b≤x
@@ -1089,7 +1130,7 @@
                  ... | 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.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) ? fc  
+                      ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b 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
@@ -1234,7 +1275,7 @@
                     ms01 {sup2} us P = MinSUP.minsup m us ?
 
 
-          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
+          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? 
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
                  --  supf0 px not is included by the chain
@@ -1258,7 +1299,7 @@
                      --                        a ≡ px → supf px ≡ px → odef U w
 
                      cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w
-                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? fc1 ⟫ where
+                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b cp fc1 ⟫ where
                          spx<b : supf0 px o< b
                          spx<b = subst (λ k → supf0 k o< b) a=px sa<b
                          cs01 : supf0 a ≡ supf0 (supf0 px)
@@ -1266,6 +1307,27 @@
                               (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
                          fc1 : FClosure A f (supf0 (supf0 px)) w
                          fc1 = subst (λ k → FClosure A f k w) cs01 fc
+                         m : MinSUP A (UnionCF A f mf ay supf0 (supf0 px))
+                         m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x))
+                         m=sa : MinSUP.sup m ≡ supf0 (supf0 px)
+                         m=sa = begin 
+                                MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x) ))  ⟩ 
+                                supf0 (supf0 px)  ∎  where open ≡-Reasoning 
+                         cp : ChainP A f mf ay supf0 (supf0 px)
+                         cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ )
+                            ; order = order 
+                            ; supu=u = sym (trans (cong supf0 (sym a=px)) cs01) } where
+                             uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 px) → FClosure A f (supf0 s) z1 
+                                 → odef (UnionCF A f mf ay supf0 (supf0 px)) z1
+                             uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<spx spx≤px 
+                                         (subst (λ k → supf0 s o< k) (sym (trans (cong supf0 (sym a=px)) cs01) ) ss<sp) fc where
+                                 s<spx : s o< supf0 px
+                                 s<spx = ZChain.supf-inject zc ss<sp 
+                                 spx≤px : supf0 px o≤ px
+                                 spx≤px = zc-b<x _ (ordtrans<-≤ spx<b b≤x)
+                             order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 px) →
+                                    FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 px)) ∨ (z1 << supf0 (supf0 px))
+                             order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) )
 
 
                      cfcs1 : odef (UnionCF A f mf ay supf0 b) w
@@ -1279,11 +1341,30 @@
                              ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x)  ⟫ )
                          ... | tri≈ ¬a sa=px ¬c with trio< a px
-                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? fc1 ⟫ where
-                             cs01 : supf0 a ≡ supf0 (supf0 a)
-                             cs01 =  sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
-                             fc1 : FClosure A f (supf0 (supf0 a)) w
-                             fc1 = subst (λ k → FClosure A f k w) cs01 fc
+                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b cp fc1 ⟫ where
+                              cs01 : supf0 a ≡ supf0 (supf0 a)
+                              cs01 =  sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
+                              fc1 : FClosure A f (supf0 (supf0 a)) w
+                              fc1 = subst (λ k → FClosure A f k w) cs01 fc
+                              m : MinSUP A (UnionCF A f mf ay supf0 (supf0 a))
+                              m = ZChain.minsup zc (o≤-refl0 sa=px)
+                              m=sa : MinSUP.sup m ≡ supf0 (supf0 a)
+                              m=sa = begin 
+                                    MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (o≤-refl0 sa=px) )  ⟩ 
+                                    supf0 (supf0 a)  ∎  where open ≡-Reasoning 
+                              cp : ChainP A f mf ay supf0 (supf0 a)
+                              cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪  A∋fc _ f mf fc  , ch-init fc ⟫ )  
+                                ; order = order 
+                                ; supu=u = sym cs01 } where
+                                 uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 a) → FClosure A f (supf0 s) z1 
+                                     → odef (UnionCF A f mf ay supf0 (supf0 a)) z1
+                                 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< (ZChain.supf-inject zc ss<sp) 
+                                         (zc-b<x _ (ordtrans<-≤ sa<b b≤x)) ss<sa fc where
+                                    ss<sa : supf0 s o< supf0 a
+                                    ss<sa = subst (λ k → supf0 s o< k ) (sym cs01) ss<sp 
+                                 order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 a) →
+                                        FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 a)) ∨ (z1 << supf0 (supf0 a))
+                                 order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) )
                          ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) )  ⟫ )
                      ... | tri≈ ¬a a=px ¬c = cfcs0 a=px