# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665372038 -32400
# Node ID e6a282eb12feb4e008966b7b7f45d7c8c9af5037
# Parent  4541c9974e53c5cadeff67cc8b0b76e8b2f0d6d8
union equal passed

diff -r 4541c9974e53 -r e6a282eb12fe src/zorn.agda
--- a/src/zorn.agda	Mon Oct 10 09:33:54 2022 +0900
+++ b/src/zorn.agda	Mon Oct 10 12:20:38 2022 +0900
@@ -448,18 +448,7 @@
 
    -- ordering is not proved here but in ZChain1 
 
-   supf-idem : {x : Ordinal } → supf x o≤ z  
-       → ¬ HasPrev A (UnionCF A f mf ay supf (supf x)) (supf x) f
-       → supf (supf x) ≡ supf x
-   supf-idem {x} sx≤z ¬np = sup=u asupf sx≤z ⟪ record { x<sup = si00  } , ¬np ⟫  where
-        ms : MinSUP A (UnionCF A f mf ay supf (supf x)) 
-        ms =  minsup sx≤z  
-        mseq : supf (supf x) ≡ MinSUP.sup ( minsup sx≤z   )
-        mseq =  supf-is-minsup sx≤z
-        si00 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf x)) w → (w ≡ supf x) ∨ (w << supf x)
-        si00 {w} uw with MinSUP.x<sup ms uw
-        ... | case1 eq = case1 (subst (λ k → w ≡ k ) ? eq)
-        ... | case2 lt = case2 (subst (λ k → w << k ) ? lt)
+   -- supf-idem : {x : Ordinal } → supf x o< z  → supf (supf x) ≡ supf x
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -1005,32 +994,50 @@
                         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 ) = ⟪ asp , ch-is-sup (supf0 px) sfpx<x
-                                   record {fcy<sup = ? ; order = zc18 ; supu=u = zc15 } (init (asupf1 {supf0 px}) zc15) ⟫ where
-                            zc15 : supf1 (supf0 px) ≡ supf0 px
-                            zc15 = ?
-                            zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
-                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
-                            zc18 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) →
-                                FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px))
-                            zc18 {s} {z1} ss<sf fc = ?
-                            zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
-                                  FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
-                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
-                                   (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
-                                mins : MinSUP A (UnionCF A f mf ay supf0 px)
-                                mins = ZChain.minsup zc o≤-refl
-                                mins-is-spx : MinSUP.sup mins ≡ supf1 px 
-                                mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
-                                s<px : s o< px
-                                s<px = supf-inject0 supf1-mono ss<spx
-                                sf≤px : supf0 s o≤ px
-                                sf≤px = subst (λ k → supf0 s o< k ) ? (ordtrans ? sfpx<x )
-                                csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
-                                csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
-                                csupf17 (init as refl ) with osuc-≡< sf≤px 
-                                ... | case2 sf<px = ZChain.csupf zc sf<px 
-                                ... | case1 sf=px = ?
+                        zc21 (init asp refl ) with  osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
+                        ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px (pxo<x op)
+                                     record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
+                              zc15 : supf1 px ≡ px
+                              zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
+                              zc14 : FClosure A f (supf1 px) (supf0 px)
+                              zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl)
+                              zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
+                              zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
+                              zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
+                                    FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
+                              zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
+                                     (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
+                                  mins : MinSUP A (UnionCF A f mf ay supf0 px)
+                                  mins = ZChain.minsup zc o≤-refl
+                                  mins-is-spx : MinSUP.sup mins ≡ supf1 px 
+                                  mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
+                                  s<px : s o< px
+                                  s<px = supf-inject0 supf1-mono ss<spx
+                                  sf<px : supf0 s o< px
+                                  sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx
+                                  csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                                  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 (ordtrans u≤x px<x) 
+                              record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫  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 (o<→≤ u≤x))) (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 (o<→≤ u≤x))) 
+                                     (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 (o<→≤ u≤x)) lt
+                                 z12 : supf1 u ≡ u
+                                 z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup)
+
 
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where