# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664673571 -32400
# Node ID 36a50c66a00dbb4682e049fc6d8ac946440c39ae
# Parent  b7fb839cdcd04479cbee4c8eafe06aac3700e4e2
...

diff -r b7fb839cdcd0 -r 36a50c66a00d src/zorn.agda
--- a/src/zorn.agda	Sat Oct 01 19:34:04 2022 +0900
+++ b/src/zorn.agda	Sun Oct 02 10:19:31 2022 +0900
@@ -891,23 +891,47 @@
                  ... | tri≈ ¬a b ¬c = px   --- supf px ≡ px
                  ... | tri> ¬a ¬b c = sp1  --- this may equal or larger then x, and sp1 ≡ supf x, is not included in UniofCF
 
+                 apx : odef A px
+                 apx = subst (λ k → odef A k ) (sym sfpx=px) ( ZChain.asupf zc )
+
                  asupf1 : {z : Ordinal } → odef A (supf1 z )
                  asupf1 {z} with trio< z px
                  ... | tri< a ¬b ¬c = ZChain.asupf zc
                  ... | tri≈ ¬a b ¬c = subst (λ k → odef A k ) (trans (cong supf0 b) (sym sfpx=px)) ( ZChain.asupf zc )
                  ... | tri> ¬a ¬b c = MinSUP.asm sup1
 
-                 -- ch1x=pchainpx : UnionCF A f mf ay supf1  x ≡ pchainpx
-                 -- ch1x=pchainpx = ?
-
-                 --  UnionCF A f mf ay supf0  x ⊆  UnionCF A f mf ay supf1  x 
-
                  zc16 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z
                  zc16 {z} z<px with trio< z px
                  ... | tri< a ¬b ¬c = refl
                  ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b))
                  ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c )
 
+                 ch1x=pchainpx : UnionCF A f mf ay supf1  x ≡ pchainpx
+                 ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where
+                      fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z 
+                      fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc
+                      fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z 
+                      fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc
+                      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 ⟫ 
+                      zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with trio< u px
+                      ... | tri< a ¬b ¬c = case1 ⟪ az , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } fc ⟫ where
+                          zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
+                          zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
+                      ... | tri≈ ¬a b ¬c = case2 fc 
+                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x  ⟫ )
+                      zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
+                      zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
+                      zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = ⟪ az , ch-is-sup u 
+                          (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) 
+                              record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 (o<→≤  u<x)) (ChainP.supu=u is-sup) } (fcpu fc (o<→≤  u<x)) ⟫  where
+                          zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
+                          zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤  u<x))) ( ChainP.fcy<sup is-sup fc )
+                      zc12 {z} (case2 fc) = ⟪  A∋fc px f mf fc , ch-is-sup px (pxo<x op) record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px)  } 
+                          (subst (λ k → FClosure A f k z ) (trans sfpx=px (sym (zc16 o≤-refl ))) fc) ⟫ where
+                          zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
+                          zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
+
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
                          tsup : MinSUP A (UnionCF A f mf ay supf1 z)
@@ -922,7 +946,7 @@
                          ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } where
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } 
 
                  supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
                  supf-mono1 {z} {w} z≤w with trio< w px