# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667640561 -32400
# Node ID cd0ef83189c5e73bc0f8db70a21eb1e94f549bc6
# Parent  39c6801887385104c531239754a390fca17b264a
...

diff -r 39c680188738 -r cd0ef83189c5 src/zorn.agda
--- a/src/zorn.agda	Sat Nov 05 13:21:42 2022 +0900
+++ b/src/zorn.agda	Sat Nov 05 18:29:21 2022 +0900
@@ -859,10 +859,30 @@
           sup1 = minsupP pchainpx pcha ptotal
           sp1 = MinSUP.sup sup1
 
+          sfpx<sp1 : supf0 px <= sp1
+          sfpx<sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
+
           --
           --     supf0 px o≤ sp1
           --
 
+          --- x ≦ supf px ≦ x ≦ sp ≦ x
+          --    x may apper any place
+
+          --  x < sp → supf x = supf px
+          --  x ≡ sp → supf x = sp 
+          --  sp < x → supf x = sp ≡ supf px
+          --      UnionCF A f mf ay supf px ⊆ UnionCF A f mf ay supf x
+
+          --  supf x does not affect UnionCF A f mf ay supf x 
+
+          --  supf px < px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
+          --  supf px ≡ px → UnionCF A f mf ay supf px ⊂ UnionCF A f mf ay supf x ≡ pchainx
+          --  x < supf px  → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
+
+          zc43 :  ( x o< sp1 ) ∨ ( sp1 o≤ x )
+          zc43 = ?
+          
           zc41 : ZChain A f mf ay x
           zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
           zc41 | (case2 sfpx<sp1) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
@@ -923,6 +943,7 @@
                  fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 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 (sf1=sf0 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 su<sx is-sup fc ⟫ = zc21 fc where
@@ -952,9 +973,10 @@
                         zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc )
                     ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b )))
                     ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc 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 su<sx is-sup fc ⟫ ) = zc21 fc where
+
+                 zc12 : {z : Ordinal} → supf0 px ≡ px → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
+                 zc12 {z} sfpx=px (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
+                 zc12 {z} sfpx=px (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
                         u<px :  u o< px
                         u<px = ZChain.supf-inject zc su<sx
                         u<x : u o< x
@@ -1001,16 +1023,13 @@
                                 s≤px : s o≤ px
                                 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
                         ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px  ⟫ )
-                 zc12 {z} (case2 fc) = zc21 fc where
+                 zc12 {z} sfpx=px (case2 fc) = zc21 fc where
                         --- supf0 px o< sp1
-                        zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px )
-                        zc20 = ?
                         zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
                         ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
-                        zc21 (init asp refl ) with  zc20
-                        ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px zc18
+                        zc21 (init asp refl ) =  ⟪ asp , ch-is-sup px zc18
                                      record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
                               zc15 : supf1 px ≡ px
                               zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
@@ -1036,28 +1055,6 @@
                                   csupf17 (init as refl ) = ZChain.csupf zc sf<px
                                   csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
 
-                        ... | case2 sfp<px  with ZChain.csupf zc sfp<px --  odef (UnionCF A f mf ay supf0 px) (supf0 px)
-                        ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫
-                        ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18
-                              record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫  where
-                                 z10 :  {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
-                                 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc)
-                                 z11  : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1
-                                      → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u )
-                                 z11 {s} {z} lt fc  = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? ))
-                                     (ChainP.order is-sup lt0 (fcup fc s≤px )) where
-                                       s<u : s o< u
-                                       s<u = supf-inject0 supf1-mono lt
-                                       s≤px : s o≤ px
-                                       s≤px = ordtrans s<u ? -- (o<→≤ u<x)
-                                       lt0 : supf0 s o< supf0 u
-                                       lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt
-                                 z12 : supf1 u ≡ u
-                                 z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup)
-                                 zc18 : supf1 u o< supf1 x
-                                 zc18 = ?
-
-
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
@@ -1101,11 +1098,11 @@
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
                      csupf2 with  trio< z1 px | inspect supf1 z1
                      csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
-                     ... | case2 lt  = zc12 (case1 cs03)  where
+                     ... | case2 lt  = zc12 ? (case1 cs03)  where
                            cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
                            cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
                      ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
-                     ... | case1 sfz=sfpx =  zc12 (case2 (init (ZChain.asupf zc) cs04 )) where
+                     ... | case1 sfz=sfpx =  zc12 ? (case2 (init (ZChain.asupf zc) cs04 )) where
                            supu=u : supf1 (supf1 z1) ≡ supf1 z1
                            supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx)
                            cs04 : supf0 px ≡ supf0 z1
@@ -1120,7 +1117,7 @@
                            cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
                            cs06 : supf0 px o< osuc px
                            cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ?
-                     csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
+                     csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
                      csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ?
                      -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )