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

diff -r 04f4baee7b68 -r 61d74b3d5456 src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 08:36:03 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 09:51:36 2022 +0900
@@ -1031,16 +1031,20 @@
 
                  fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
                  fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px
-                 ... | tri< a<px ¬b ¬c = ? -- chain-mono ZChain.fcs<sup a
+                 ... | 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  
+                      ... | ⟪ 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 
                       px<b : px o< b
                       px<b = subst₂ (λ j k → j o< k) a=px refl a<b
                       b=x : b ≡ x
                       b=x with trio< b x
-                      ... | tri< a ¬b ¬c = ?
+                      ... | 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<> c ? ) -- subst₂ (λ j k → j o≤ k ) ? ? a<b 
-                 ... | tri> ¬a ¬b c = ? --  px o< a o< b o≤ x
+                      ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
+                 ... | 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
                  zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫