# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668783253 -32400
# Node ID 2808471040c06bb47f7190fb6cd4d75cf3b88790
# Parent  5c62c97adac9181c174c84b75c6bb072786a7046
...

diff -r 5c62c97adac9 -r 2808471040c0 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 18 19:37:18 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 23:54:13 2022 +0900
@@ -431,7 +431,7 @@
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
            → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b
       cfcs : (mf< : <-monotonic-f A f)
-         {a b w : Ordinal } → a o< b → b o≤ z → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
+         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< z  → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -441,15 +441,6 @@
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x)
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
 
-   -- cfcs implirs supf-mono and supf-<
-   -- ¬ ( HasPreb A A f (supf b)
-   -- supf-mono' : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-   -- supf-mono' {x} {y} x≤y with osuc-≡< x≤y
-   -- ... | case1 eq = o≤-refl0 ( cong supf eq )
-   -- ... | case2 lt with cfcs lt ? (init asupf refl)
-   -- ... | ⟪ ua , ch-init fc ⟫ = ?
-   -- ... | ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?
-
    chain : HOD
    chain = UnionCF A f mf ay supf z
    chain⊆A : chain ⊆' A
@@ -492,9 +483,12 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
+   supf<A : {x : Ordinal } → supf x o< & A
+   supf<A = z09 asupf
+
    csupf : (mf< : <-monotonic-f A f) {b : Ordinal } 
-      → supf b o< supf z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
-   csupf mf< {b} sb<sz = cfcs mf< (supf-inject sb<sz) o≤-refl (init asupf refl)
+      → supf b o< supf z → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+   csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
 
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
    fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
@@ -517,6 +511,20 @@
        fsp≤sp : f sp <=  sp
        fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
 
+   csupf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o< z  → supf (supf b) ≡ supf b
+   csupf-idem  mf< {b} b≤z sfb<x = z52 where
+       z54 :  {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
+       z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
+       z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) 
+                   (sym (supf-is-minsup b≤z)) 
+                   (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z su<z fc )) where
+               u<b : u o< b
+               u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x )
+               su<z : supf u o< z
+               su<z = subst (λ k → k o< z ) (sym (ChainP.supu=u is-sup)) ( ordtrans<-≤ u<b b≤z )
+       z52 : supf (supf b) ≡ supf b
+       z52 = sup=u asupf (o<→≤ sfb<x) ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
+
 UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
         → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
@@ -698,7 +706,7 @@
                 s<z : s o< & A
                 s<z = ordtrans s<b b<z
                 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc mf< (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z)))
+                zc04 = ZChain.csupf zc mf< (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z))) (ZChain.supf<A zc)
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
@@ -760,7 +768,7 @@
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.cfcs zc mf< b<x x≤A  fc
+                          m13 = ZChain.cfcs zc mf< b<x x≤A (ZChain.supf<A zc) fc
 
         ... | no lim = record { is-max = is-max ; order = order }  where
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
@@ -798,7 +806,7 @@
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.cfcs zc mf< b<x x≤A  fc
+                          m13 = ZChain.cfcs zc mf< b<x x≤A (ZChain.supf<A zc) fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -823,22 +831,6 @@
            ax : odef A x
            is-sup : IsMinSUP A B f ax
 
-     supf-fc : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → Ordinal  → Ordinal
-     supf-fc f mf {y} ay x = TransFinite0 ind x where
-            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → Ordinal ) → Ordinal
-            ind x prev  with trio< x o∅ 
-            ... | tri< a ¬b ¬c = ?
-            ... | tri≈ ¬a b ¬c = MinSUP.sup (ysup f mf ay)
-            ... | tri> ¬a ¬b 0<x with Oprev-p x
-            ... | yes op = ? where
-                px = Oprev.oprev  op
-                sfc00 : Ordinal
-                sfc00 with trio< (prev px ? ) (MinSUP.sup (ysup f mf ? ))
-                ... | tri< a ¬b ¬c = ?
-                ... | tri≈ ¬a b ¬c = ?
-                ... | tri> ¬a ¬b c = ?
-            ... | no lim = ?
-
      --
      -- create all ZChains under o< x
      --
@@ -939,34 +931,16 @@
           --     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 : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
           zc43 x with trio< x sp1
           ... | tri< a ¬b ¬c = case1 a
           ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
           ... | tri> ¬a ¬b c = case2 (o<→≤ c)
-          
+
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?  }  where
-                 --  supf0 px is included in the chain of sp1
-                 --  supf0 px ≡ px ∧ supf0 px o< sp1 → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
-                 --     else                             UnionCF A f mf ay supf0 px  ≡ UnionCF supf1 x
-                 --  supf1 x ≡ sp1, which is not included now
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px
@@ -1033,13 +1007,19 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
+                 --  supf0 a ≡ px we cannot use previous cfcs
+                 --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
+                 --    supf0 a o< sp1 ≡ x
+                 --    sp1 ≡ px ≡ supf0 a o< x
+                 --    sp1 o< px ≡ supf0 a → ⊥
+                 -- 
                  cfcs : (mf< : <-monotonic-f A f) {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
-                 cfcs mf< {a} {b} {w} a<b b≤x fc with trio< a px
+                     → a o< b → b o≤ x → supf1 a o< x  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<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 osuc-≡< b≤x
-                      ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) fc  
+                      ... | case2 lt with ZChain.cfcs zc mf< 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<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
@@ -1053,7 +1033,7 @@
                                    (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.cfcs zc mf< a<px o≤-refl fc  
+                      z50 | case1 eq with ZChain.cfcs zc mf< 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
@@ -1090,7 +1070,7 @@
                           z54 {z} ⟪ az , ch-init fc ⟫ = ZChain.fcy<sup zc o≤-refl fc
                           z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = subst (λ k → (z ≡ k) ∨ (z << k )) 
                                        (sym (ZChain.supf-is-minsup zc o≤-refl)) 
-                                       (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< u<px o≤-refl fc )) where
+                                       (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< u<px o≤-refl ? fc )) where
                                    u<px : u o< px
                                    u<px = ZChain.supf-inject zc ( subst (λ k → k o< supf0 px) (sym (ChainP.supu=u is-sup)) u<b )
                           -- u<b    : u o< supf0 px
@@ -1105,7 +1085,7 @@
                           order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
                                    (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
                                    (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                       spx≤px (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) )))
+                                       spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) )))
                           cp1 : ChainP A f mf ay supf1 spx
                           cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) 
                                   ( ZChain.fcy<sup zc spx≤px fc )
@@ -1186,44 +1166,21 @@
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?    }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
                  --  supf0 px not is included by the chain
                  --     supf1 x ≡ supf0 px because of supfmax
 
-                 supf1 : Ordinal → Ordinal
-                 supf1 z with trio< z px
-                 ... | tri< a ¬b ¬c = supf0 z
-                 ... | tri≈ ¬a b ¬c = supf0 z
-                 ... | tri> ¬a ¬b c = supf0 px
-
-                 sf1=sf0 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z
-                 sf1=sf0 {z} z<px with trio< z px
-                 ... | tri< a ¬b ¬c = refl
-                 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
-
-                 sf=eq :  { z : Ordinal } → z o< x → supf0 z ≡ supf1 z
-                 sf=eq {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = refl
-                 ... | tri≈ ¬a b ¬c = refl 
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op))  z<x ⟫ )
-                 sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
-                 sf≤ {z} x≤z with trio< z px
-                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
-                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
-                 ... | tri> ¬a ¬b c = o≤-refl0 ( ZChain.supfmax zc px<x )
-
-                 sf=eq0 :  { z : Ordinal } → z o< x → supf1 z ≡ supf0 z
-                 sf=eq0 {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = refl
-                 ... | tri≈ ¬a b ¬c = refl 
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op))  z<x ⟫ )
-                 sf≤0 :  { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z
-                 sf≤0 {z} x≤z with trio< z px
-                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
-                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
-                 ... | tri> ¬a ¬b c = o≤-refl0 ? -- (sym ( ZChain.supfmax zc px<x ))
+                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                     → a o< b → b o≤ x →  supf0 a o< x → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< b px 
+                 ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) ? fc
+                 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl ? fc
+                 ... | tri> ¬a ¬b px<b with trio< a px
+                 ... | tri< a ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) ( ZChain.cfcs zc mf< a o≤-refl ? fc )
+                 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c )
+                 ... | tri≈ ¬a refl ¬c = ? --  supf0 px o< x  → odef (UnionCF A f mf ay supf0 x) (supf0 px)
+                                           --  x o≤ supf0 px o≤ sp  →
 
                  zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
                  zc17 {z} with trio< z px
@@ -1233,88 +1190,10 @@
                       zc177 : supf0 z ≡ supf0 px
                       zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
 
-                 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
-                 supf-mono1 {z} {w} z≤w with trio< w px
-                 ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w )
-                 ... | tri≈ ¬a refl ¬c with trio< z px
-                 ... | tri< a ¬b ¬c = zc17
-                 ... | tri≈ ¬a refl ¬c = o≤-refl
-                 ... | tri> ¬a ¬b c = o≤-refl
-                 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b px<w with trio< z px
-                 ... | tri< a ¬b ¬c = zc17
-                 ... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)  -- z=px   supf1 z = supf0 z, supf1 w = supf0 px
-                 ... | tri> ¬a ¬b c = o≤-refl
-
-                 pchain1 : HOD
-                 pchain1 = UnionCF A f mf ay supf1 x
-
-                 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
-                 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ?  ?  ⟫
-
-                 zc111 : {z : Ordinal} → z o< px → OD.def (od pchain1) z → OD.def (od pchain) z
-                 zc111 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                 zc111 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ?  ?  ⟫
-
-                 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) f x ) ∨  (HasPrev A pchain f x )
-                        → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
-                 zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
-                 zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px
-                 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 ? ? fc  ⟫
-                 ... | tri≈ ¬a eq ¬c  = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 ? ⟫ where
-                        s1u=u : supf0 u1 ≡ u1
-                        s1u=u = ? -- ChainP.supu=u u1-is-sup
-                        zc12 : supf0 u1 ≡ px
-                        zc12 = trans s1u=u eq
-                 zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
-                        eq : u1 ≡ x
-                        eq with trio< u1 x
-                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
-                        ... | tri≈ ¬a b ¬c = b
-                        ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? )
-                        s1u=x : supf0 u1 ≡ x
-                        s1u=x = trans ? eq
-                        zc13 : osuc px o< osuc u1
-                        zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) )
-                        x≤sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
-                        x≤sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
-                        x≤sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? ))
-                        ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where
-                                 zc14 : u ≡ osuc px
-                                 zc14 = begin
-                                    u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩
-                                    supf0 u ≡⟨ ? ⟩
-                                    supf0 u1 ≡⟨ s1u=x ⟩
-                                    x ≡⟨ sym (Oprev.oprev=x op) ⟩
-                                    osuc px ∎ where open ≡-Reasoning
-                        ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
-                        zc12 : supf0 x ≡ u1
-                        zc12 = subst  (λ k → supf0 k ≡ u1) eq ?
-                        zcsup : xSUP (UnionCF A f mf ay supf0 px) f x
-                        zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
-                                 ; is-sup = record { x≤sup = x≤sup ; minsup = ? } }
-                 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
-                        eq : u1 ≡ x
-                        eq with trio< u1 x
-                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
-                        ... | tri≈ ¬a b ¬c = b
-                        ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? )
-                        zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
-                        zc20 {z} (init asu su=z ) = zc13 where
-                          zc14 : x ≡ z
-                          zc14 = begin
-                             x ≡⟨ sym eq ⟩
-                             u1 ≡⟨  sym ? ⟩
-                             supf0 u1 ≡⟨ su=z ⟩
-                             z ∎ where open ≡-Reasoning
-                          zc13 : odef pchain z
-                          zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) )
-                        zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 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)
-                         tsup=sup : supf1 z ≡ MinSUP.sup tsup
+                         tsup : MinSUP A (UnionCF A f mf ay supf0 z)
+                         tsup=sup : supf0 z ≡ MinSUP.sup tsup
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px
@@ -1327,9 +1206,7 @@
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc32 = ZChain.sup zc o≤-refl
                      zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 ne {w} lt with zc11 ? ⟪ proj1 lt , ? ⟫
-                     ... | case1 lt = SUP.x≤sup zc32 lt
-                     ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
+                     zc34 ne {w} lt = ?
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
                      zc36 : ¬ (supf0 px ≡ px) → STMP z≤x