# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668672287 -32400
# Node ID 908369b2d08b8082d51d04002273d200b0eeb8d9
# Parent  61d74b3d54560dbb75498b9a290662cb24d554e4
...

diff -r 61d74b3d5456 -r 908369b2d08b src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 09:51:36 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 17:04:47 2022 +0900
@@ -1033,10 +1033,36 @@
                  fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
                       z50 : odef (UnionCF A f mf ay supf1 b) w
-                      z50 with ZChain.fcs<sup zc a<px o≤-refl fc  
+                      z50 with osuc-≡< b≤x
+                      ... | case2 lt with ZChain.fcs<sup zc 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<x is-sup fc ⟫ = ⟪ az , ch-is-sup u ? ? ? ⟫ 
-                 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b ? ? ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 
+                      ... | ⟪ 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 b≤x )
+                           u<x : u o< 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) 
+                                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) 
+                                   (sym (sf=eq u<x)) s<u)  
+                                    (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
+                               ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
+                      z50 | case1 eq with ZChain.fcs<sup zc a<px o≤-refl fc  
+                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                      ... | ⟪ 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
+                           u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc )
+                           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) 
+                                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) 
+                                   (sym (sf=eq u<x)) s<u)  
+                                    (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
+                               ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
+                 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b cp1 z51 ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 
                       px<b : px o< b
                       px<b = subst₂ (λ j k → j o< k) a=px refl a<b
                       b=x : b ≡ x
@@ -1044,6 +1070,12 @@
                       ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) --  px o< b o< x
                       ... | tri≈ ¬a b ¬c = b
                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
+                      z51 : FClosure A f (supf1 px) w
+                      z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
+                      cp1 : ChainP A f mf ay supf1 px
+                      cp1 = record { fcy<sup = λ {z} fc → ? 
+                               ; order =  λ {s} {z} s<u fc  → ? 
+                               ; supu=u = ? }
                  ... | 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 mf ay supf1 x) z → odef pchainpx z
@@ -1088,7 +1120,7 @@
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
-                    ms01 {sup2} us P = MinSUP.minsup m ? ?
+                    ms01 {sup2} us P = MinSUP.minsup m us ?
                  ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
@@ -1096,7 +1128,7 @@
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
-                    ms01 {sup2} us P = MinSUP.minsup m ? ?
+                    ms01 {sup2} us P = MinSUP.minsup m us ?
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
                     m = sup1
@@ -1104,7 +1136,7 @@
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
-                    ms01 {sup2} us P = MinSUP.minsup m ? ?
+                    ms01 {sup2} us P = MinSUP.minsup m us ?
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?