# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665305921 -32400
# Node ID 6146d75131f51c55a2cbb89efb654b9a537fd4b7
# Parent  ac4daa43ef2a8447a0010b860b7cb608ed6ee028
...

diff -r ac4daa43ef2a -r 6146d75131f5 src/zorn.agda
--- a/src/zorn.agda	Fri Oct 07 17:13:41 2022 +0900
+++ b/src/zorn.agda	Sun Oct 09 17:58:41 2022 +0900
@@ -656,14 +656,6 @@
              = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
-              sb≤sx : supf b o≤ supf x
-              sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 
-              sb<sx : supf b o< supf x
-              sb<sx with osuc-≡< sb≤sx
-              ... | case2 lt = lt
-              ... | case1 sb=sx = ? where
-                  -- b ≡ x
-                  -- b o< px → a < * b → odef (UnionCF A f mf ay supf px) b
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
@@ -687,10 +679,6 @@
            is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
            ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
-              sb≤sx : supf b o≤ supf x
-              sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) 
-              sb<sx : supf b o< supf x
-              sb<sx = ?
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
@@ -821,14 +809,6 @@
           pchain  : HOD
           pchain   = UnionCF A f mf ay supf0 px
 
-          -- px o< supf0 px → UnionCF supf0 px ≡ UnionCF supf1 x 
-          --       supf1 x ≡ supf0 px
-          -- px ≡  supf0 px → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 
-          --       supf1 x ≡ sup of ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) (= UnionCF supf1 x)))  -- nsup ≥ supf0 px 
-          -- supf0 px o< px → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 
-          --         nsup o≥ supf0 px → supf1 x ≡ nsup
-          --         nsup o< supf0 px → ?
-
           supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b 
           supf-mono = ZChain.supf-mono zc
 
@@ -840,18 +820,12 @@
           ... | case1 eq = case2 eq
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
-          zc4 : ZChain A f mf ay x     --- supf px ≤ supf x
-          zc4 with trio< x (supf0 px)
-          ... | tri> ¬a ¬b c =  record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
-          ... | tri≈ ¬a b ¬c =  ? where
-          -- ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
-          --    ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
-  
-                 --  we are going to determine (supf x), which is not specified in previous zc
-                 --  case1 : supf px ≡ px 
-                 --     supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and  FClosure px 
-                 sfpx=px = ?
+          zc41 : supf0 px o≤ x →  ZChain A f mf ay x 
+          zc41 sfpx≤x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
+                 --  supf0 px is included by the chain
+                 --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 
+                 --  supf1 x ≡ sp1, which is not included now
 
                  pchainpx : HOD
                  pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
@@ -865,7 +839,7 @@
                  zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b
                  zc02 {a} {b} ca fb = zc05 fb where
                     zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
-                    zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) (sym sfpx=px)
+                    zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ?
                     zc05 : {b : Ordinal } → FClosure A f px b → a <= b
                     zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb ))
                     ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
@@ -894,249 +868,94 @@
                       lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
                  ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b)
 
-                 sup1 : MinSUP A pchainpx 
-                 sup1 = minsupP pchainpx zc01 ptotal
+                 pcha : pchainpx ⊆' A
+                 pcha (case1 lt) = proj1 lt
+                 pcha (case2 fc) = A∋fc _ f mf fc
 
-                 sp1 : Ordinal
-                 sp1 = MinSUP.sup sup1 
+                 sup1 : MinSUP A pchainpx 
+                 sup1 = minsupP pchainpx pcha ptotal
+                 sp1 = MinSUP.sup sup1
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
-                 ... | 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
+                 ... | tri≈ ¬a b ¬c = supf0 z 
+                 ... | tri> ¬a ¬b c = sp1
 
                  sf1=sf0 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z
-                 sf1=sf0 {z} z<px with trio< z px
+                 sf1=sf0 {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 )
+                 ... | tri≈ ¬a b ¬c = refl
+                 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
 
-                 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 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w )
-                 ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w 
-                 ... | case1 refl = o≤-refl0 zc17 where
-                       zc17 : supf1 px ≡ px
-                       zc17 with trio< px px
-                       ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-                       ... | tri≈ ¬a b ¬c = refl
-                       ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl )
-                 ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ lt))) (sym sfpx=px) ( supf-mono z≤w )
-                 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
-                 ... | tri< a ¬b ¬c = zc19 where
-                       zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
-                       zc21 = ZChain.minsup zc (o<→≤ a)
-                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a) ux))
-                       zc19 : supf0 z o≤ sp1 
-                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
-                 ... | tri≈ ¬a b ¬c = zc18 where
-                       zc21 : MinSUP A (UnionCF A f mf ay supf0 z)
-                       zc21 = ZChain.minsup zc (o≤-refl0 b)
-                       zc20 : MinSUP.sup zc21 ≡ px
-                       zc20 = begin
-                         MinSUP.sup zc21 ≡⟨ sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) ⟩
-                         supf0 z ≡⟨ cong supf0 b ⟩
-                         supf0 px ≡⟨ sym sfpx=px ⟩
-                         px ∎ where open ≡-Reasoning
-                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux))
-                       zc18 : px o≤ sp1 -- supf0 z ≡ px 
-                       zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
-                 ... | tri> ¬a ¬b c = o≤-refl
-
-                 supf-<1 : {z0 z1 : Ordinal} → supf1 z0 o< supf1 z1 → supf1 z0 << supf1 z1
-                 supf-<1 {z0} {z1} sz0<sz1 = zc21 where
-                        z0<z1 :  z0 o< z1
-                        z0<z1 = supf-inject0 supf-mono1 sz0<sz1
-                        zc26 : supf0 px <= sp1
-                        zc26 with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl ))
-                        ... | case1 eq = case1 (trans (sym sfpx=px) eq  )
-                        ... | case2 lt = case2 (subst (λ k → k << sp1 ) sfpx=px lt)
-                        zc22 : ¬ px ≡ sp1 → supf0 px << sp1
-                        zc22 not with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl ))
-                        ... | case1 eq = ⊥-elim ( not eq )  -- px ≡ sp1
-                        ... | case2 lt = subst (λ k → k << sp1 ) sfpx=px lt
-                        zc21 : supf1 z0 << supf1 z1
-                        zc21 with trio< z1 px
-                        ... | tri< a ¬b ¬c = subst (λ k → k << supf0 z1) (sym (sf1=sf0 (o<→≤ (ordtrans z0<z1 a))))
-                           ( ZChain.supf-< zc (subst (λ k → k o< supf0 z1) (sf1=sf0 (o<→≤ (ordtrans z0<z1 a))) sz0<sz1 ))
-                        ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j << k ) (sym (sf1=sf0 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 )))) (sym sfpx=px)
-                           ( ZChain.supf-< zc (subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 ))) sfpx=px sz0<sz1 ))
-                        ... | tri> ¬a ¬b px<z1 with trio< z0 px   --- supf1 z1 ≡ sp1
-                        ... | tri< a ¬b ¬c = zc23 where  
-                              zc23 : supf0 z0 << sp1
-                              zc23 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ a) )
-                              ... | case1 eq = subst (λ k → k << sp1 ) (sym eq) (zc22 zc24) where
-                                  zc25 : px ≡ sp1 → supf0 z0 ≡ sp1
-                                  zc25 px=sp1 = begin supf0 z0 ≡⟨ eq ⟩
-                                     supf0 px ≡⟨ sym ( sfpx=px ) ⟩
-                                     px ≡⟨ px=sp1 ⟩
-                                     sp1 ∎ where open ≡-Reasoning
-                                  zc24 : ¬ px ≡ sp1
-                                  zc24 eq1 = ⊥-elim (o<¬≡ (zc25 eq1) sz0<sz1 )
-                              ... | case2 lt with zc26
-                              ... | case1 eq = subst (λ k → supf0 z0 << k ) eq (ZChain.supf-< zc lt) 
-                              ... | case2 lt1 = ptrans (ZChain.supf-< zc lt) lt1
-                        ... | tri≈ ¬a b ¬c = subst (λ k → k << sp1 ) (sym sfpx=px) (zc22 zc23 ) where
-                              zc23 : ¬ px ≡ sp1
-                              zc23 eq = ⊥-elim (o<¬≡  eq sz0<sz1 )
-                        ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl sz0<sz1 )
+                 sf1=sp1 : {z : Ordinal } → px o< z → supf1 z ≡ sp1
+                 sf1=sp1 {z} px<z with trio< z px
+                 ... | tri< a ¬b ¬c = ⊥-elim ( o<> px<z a )
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z )
+                 ... | tri> ¬a ¬b c = refl
 
-                 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 ) (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 u≤x is-sup fc ⟫ = zc21 fc where
-                          zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
-                          zc21 {z1} (fsuc z2 fc ) with zc21 fc
-                          ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
-                          ... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
-                          ... | case2 fc = case2 (fsuc _ fc) 
-                          zc21 (init asp refl ) with trio< u px | inspect supf1 u
-                          ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17
-                                 ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where
-                              zc17 :  {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u →
-                                    FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                              zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup 
-                                 (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where
-                                    zc19 : u o≤ px
-                                    zc19 = o<→≤ a
-                                    zc18 : s o≤ px
-                                    zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19
-                              zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
-                              zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
-                          ... | tri≈ ¬a b ¬c | _ = case2 (init apx refl )
-                          ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ?  ⟫ )
-                      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 ⟫ ) = zc21 fc where
-                          zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) 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 trio< u px | inspect supf1 u
-                          ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u 
-                               ? -- (subst (λ k → u o< k) (Oprev.oprev=x op) ?) 
-                                  record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans ((sf1=sf0 ?)) (ChainP.supu=u is-sup) } zc14 ⟫  where
-                              zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
-                                    FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
-                              zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 ?)) ( ChainP.order is-sup 
-                                 (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ?) ss<spx) (fcup fc s≤px) ) where
-                                    s≤px : s o≤ px
-                                    s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u≤x)
-                              zc14 : FClosure A f (supf1 u) (supf0 u)
-                              zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?)
-                              zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
-                              zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ?)) ( ChainP.fcy<sup is-sup fc )
-                          ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 
-                                ; order = zc17 ; supu=u = zc18   } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b)))  ) ⟫ where
-                              zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px )
-                              zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc )
-                              zc18 : supf1 px ≡ px
-                              zc18 = begin
-                                  supf1 px ≡⟨ sf1=sf0 o≤-refl ⟩
-                                  supf0 px ≡⟨ cong supf0 (sym b) ⟩
-                                  supf0 u ≡⟨ ChainP.supu=u is-sup ⟩
-                                  u ≡⟨ b ⟩
-                                  px ∎ where open ≡-Reasoning
-                              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)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl)))
-                                ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where
-                                  zc19 : supf1 px ≡ supf0 u
-                                  zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
-                                  s≤px : s o≤ px
-                                  s≤px = o<→≤ (supf-inject0 supf-mono1 ss<spx)
-                          ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ?   ⟫ )
-                      zc12 {z} (case2 fc) = zc21 fc where
-                          zc21 : {z1 : Ordinal } → FClosure A f 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 ) = ⟪ asp , ch-is-sup px ?
-                                     record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
-                              zc15 : supf1 px ≡ px
-                              zc15 = trans (sf1=sf0 o≤-refl ) (sym sfpx=px)
-                              zc14 : FClosure A f (supf1 px) px
-                              zc14 = init (subst (λ k → odef A k) (sym zc15) asp) 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 )
-                              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 supf-mono1 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) (sym sfpx=px)) ss<spx
-                                  -- (sf1=sf0 ?) (trans ? 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)
+                 supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
+                 supf1-mono {a} {b} a≤b with trio< b px 
+                 ... | tri< a ¬b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ (ordtrans≤-< a≤b a)))) refl ( supf-mono a≤b )
+                 ... | tri≈ ¬a b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (subst (λ k → a o≤ k) b a≤b))) refl ( supf-mono a≤b )
+                 supf1-mono {a} {b} a≤b | tri> ¬a ¬b c with trio< a px
+                 ... | tri< a<px ¬b ¬c = zc19 where
+                       zc21 : MinSUP A (UnionCF A f mf ay supf0 a)
+                       zc21 = ZChain.minsup zc (o<→≤ a<px)
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a<px) ux ) )
+                       zc19 : supf0 a o≤ sp1 
+                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
+                 ... | tri≈ ¬a b ¬c = zc18 where
+                       zc21 : MinSUP A (UnionCF A f mf ay supf0 a)
+                       zc21 = ZChain.minsup zc (o≤-refl0 b)
+                       zc20 : MinSUP.sup zc21 ≡ supf0 a
+                       zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) 
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux ) )
+                       zc18 : supf0 a o≤ sp1 
+                       zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
+                 ... | tri> ¬a ¬b c = o≤-refl
 
                  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 : MinSUP A (UnionCF A f mf ay supf0 z)
                          tsup=sup : supf1 z ≡ MinSUP.sup tsup 
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px 
                  ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a))  } where
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
                  ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (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 = ? } 
+                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
+                         ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } 
 
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                  csupf1 {z1} sz1<x with trio< (supf0 z1) px
-                 ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) (sym (sf1=sf0 z1≤px)) (case1 (ZChain.csupf zc a )) where
+                 ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) ? (sym (sf1=sf0 (o<→≤ a) )) (case1 (ZChain.csupf zc a )) where
                         z1≤px : z1 o≤ px
-                        z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
-                 ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
-                      z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px 
-                      z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ))
-                      zc20 : supf0 px ≡ supf1 z1 
-                      zc20 = begin
-                        supf0 px  ≡⟨ sym sfpx=px ⟩
-                        px  ≡⟨ sym b ⟩
-                        supf0 z1  ≡⟨ sym (sf1=sf0 z1≤px)  ⟩
-                        supf1 z1 ∎ where open ≡-Reasoning
+                        z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) ? a ))
+                 ... | tri≈ ¬a b ¬c = ?
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc21 , subst (λ k → z1 o< k ) (sym (Oprev.oprev=x op)) zc22 ⟫ ) where
                       zc21 : px o< z1
-                      zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c  )
+                      zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) ? c  )
                       zc22 : z1 o< x -- c : px o< supf0 z1
-                      zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )
+                      zc22 = ? -- supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )
                      -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
 
-          ... | tri< a ¬b ¬c = ? where
+          zc4 : ZChain A f mf ay x     --- supf px ≤ supf x
+          zc4 with trio< x (supf0 px)
+          ... | tri> ¬a ¬b c = zc41 (o<→≤ c)
+          ... | tri≈ ¬a b ¬c = zc41 (o≤-refl0 (sym b))
+          ... | tri< a ¬b ¬c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
 
-                 --  case2 : px o< supf px 
-                 --     supf px is not MinSUP of previous chain , supf x ≡ supf px
+                 --  supf0 px not is included by the chain
+                 --     supf1 x ≡ supf0 px because of supfmax
 
-            -- record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
-            --              ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z