# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668185365 -32400
# Node ID 0d8dafbecb0d83cd475db03869e70b84beb03bd8
# Parent  94357ced682dcfa9b4082668c4540e67c00fe7dc
zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x  → ¬ ( c << x ) ?

diff -r 94357ced682d -r 0d8dafbecb0d src/zorn.agda
--- a/src/zorn.agda	Wed Nov 09 03:14:40 2022 +0900
+++ b/src/zorn.agda	Sat Nov 12 01:49:25 2022 +0900
@@ -418,7 +418,7 @@
 
       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 )
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+      csupf : {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
 
    chain : HOD
    chain = UnionCF A f mf ay supf z
@@ -666,7 +666,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 (z09 (ZChain.asupf zc))
+                zc04 = ZChain.csupf zc ? -- (z09 (ZChain.asupf zc))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
@@ -995,152 +995,6 @@
                     ... | 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  ⟫ )
 
-                 zc35 : {z : Ordinal} → ¬ (supf0 px ≡ px) → odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
-                 zc35 {z} ne ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ 
-                 zc35 {z} ne ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) )
-                 ... | case1 eq = zc34 where
-                      u<x0 : u o≤ px
-                      u<x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono u<x )
-                      zc34 : odef (UnionCF A f mf ay supf0 x) z
-                      zc34 with trio< (supf0 px) px
-                      ... | tri< sf0px<px ¬b ¬c = cp3 ( subst ( λ k → FClosure A f k z) 
-                          (trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where 
-                              cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z
-                              cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px)
-                              cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc)
-                      ... | tri≈ ¬a b ¬c = ⊥-elim (ne b)
-                      ... | tri> ¬a ¬b px<sf0px = ⊥-elim (¬p<x<op ⟪ cp5 , cp4 ⟫ ) where
-                           cp4 : u o< osuc px
-                           cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono u<x  )
-                           cp5 : px o< u
-                           cp5 = subst (λ k → px o< k ) ( begin
-                             supf0 px ≡⟨ sym (ZChain.supfmax zc px<x)  ⟩
-                             supf0 x  ≡⟨ sym eq  ⟩
-                             supf0 u  ≡⟨ sym (sf1=sf0 u<x0)  ⟩
-                             supf1 u  ≡⟨ ChainP.supu=u is-sup  ⟩
-                             u ∎  ) px<sf0px  where open ≡-Reasoning 
-                 ... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where
-                      u<x0 : u o< x
-                      u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤  px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px
-                      sf0u=sf1u : supf0 u ≡ supf1 u
-                      sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))
-                      cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s
-                      cp2 {s} ss<su = sym ( sf1=sf0 ( begin
-                             s  <⟨ ZChain.supf-inject zc ss<su ⟩
-                             u  ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0  ⟩
-                             px ∎ )) where open o≤-Reasoning O
-                      fc1 : FClosure A f (supf0 u) z
-                      fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc
-                      cp1 : ChainP A f mf ay supf0 u
-                      cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc )  
-                           ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u)
-                              (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u)  
-                                (subst (λ k → FClosure A f k z ) (cp2 s<u) fc ))
-                           ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup)  }
-
-                 zc33 : {z : Ordinal} → ¬ (supf0 px o< sp1) → odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
-                 zc33 {z} lt = UChain⊆ A f mf ay supf1-mono (λ lt → sym (sf=eq lt)) sf≤0  where
-                     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 px<z with trio< sp1 (supf0 x) -- = ?   --- sp1 o≤ supf0 x
-                     ... | tri< a ¬b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) 
-                           (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) ( o<→≤ a  )
-                     ... | tri≈ ¬a b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) 
-                           (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z)))  (o≤-refl0 b)
-                     ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 ))
-
-                 3cases : (¬ (supf0 px ≡ px)) ∨ ( ¬ (supf0 px o< sp1 )) ∨ ( (supf0 px ≡ px) ∧  (supf0 px o< sp1 )) 
-                 3cases with o≡? (supf0 px) px
-                 ... | no ne = case1 ne
-                 ... | yes eq with trio< (supf0 px) sp1
-                 ... | tri< a ¬b ¬c = case2 (case2 ⟪ eq , a ⟫ )
-                 ... | tri≈ ¬a b ¬c = case2 (case1 ¬a )
-                 ... | tri> ¬a ¬b c = case2 (case1 ¬a )
-
-                 zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
-                 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
-                 zc12 {z} sfpx=px sfpx<sp (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
-                        u<x = ordtrans u<px px<x
-                        u≤px : u o≤ px
-                        u≤px = o<→≤ u<px
-                        s1u<s1x : supf1 u o< supf1 x
-                        s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) su<sx) (supf1-mono (o<→≤ px<x) )
-                        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
-                             s1u<s1x
-                                record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (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<su fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<px))) ( ChainP.order is-sup
-                               (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<px)) ss<su) (fcup fc s≤px) ) where
-                                  s≤px : s o≤ px -- ss<su : supf1 s o< supf1 u
-                                  s≤px = ordtrans ( supf-inject0 supf1-mono ss<su ) (o<→≤ u<px)
-                            zc14 : FClosure A f (supf1 u) (supf0 u)
-                            zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px)
-                            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 u≤px )) ( ChainP.fcy<sup is-sup fc )
-                        ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (subst (λ k → supf1 k o< supf1 x) b s1u<s1x)  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 supf1-mono ss<spx)
-                        ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px  ⟫ )
-                 zc12 {z} sfpx=px sfpx<sp (case2 fc) = zc21 fc where
-                        --- supf0 px o< sp1
-                        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 ) =  ⟪ 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)
-                              zc18 : supf1 px o< supf1 x  
-                              zc18 = subst₂ ( λ j k → j o< k ) (sym (sf1=sf0 o≤-refl)) (sym (sf1=sp1 px<x)) sfpx<sp
-                              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 (zc25 (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
-                                  zc25 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
-                                  zc25 (init as refl ) = ZChain.csupf zc sf<px
-                                  zc25 (fsuc x fc) = ZChain.f-next zc (zc25 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)
@@ -1177,59 +1031,11 @@
                  csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) (
                        UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ 
                          (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) 
-                         (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
+                         (ZChain.csupf zc ? ))) -- (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
                  -- px o< z1 , px o≤ supf1 z1  -->   px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1
 
-                 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                 csupf1 {z1} sz1<x = csupf2 where
-                     --  z1 o< px → supf1 z1 ≡ supf0 z1
-                     --  z1 ≡ px , supf0 px o< px   .. px o< z1, x o≤ z1 ...  supf1 z1 ≡ sp1
-                     --  z1 ≡ px , supf0 px ≡  px
-                     psz1≤px :  supf1 z1 o≤ px
-                     psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
-                     csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                     csupf2 with 3cases
-                     ... | case2 (case2 p) with  trio< z1 px | inspect supf1 z1
-                     ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
-                     ... | case2 lt  = zc12 (proj1 p) (proj2 p) (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 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where
-                           cs04 : supf0 px ≡ supf0 z1
-                           cs04 = begin
-                             supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
-                             supf1 px ≡⟨ sym sfz=sfpx ⟩
-                             supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a)  ⟩
-                             supf0 z1 ∎ where open ≡-Reasoning
-                     ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫  )  where
-                            --- supf1 z1 ≡ px , z1 o< px ,  px ≡ supf0 z1 o< supf0 px o< x
-                           cs05 : px o< supf0 px
-                           cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
-                           cs06 : supf0 px o< osuc px
-                           cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x
-                     csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (proj1 p) (proj2 p) 
-                           (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
-                     csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } =  ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where
-                           cs08 : px o< sp1
-                           cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p )
-                           cs09 : sp1 o< osuc px
-                           cs09  = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
-                     csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 --  ¬ (supf0 px o< sp1  --  sp1 o≤ supf px)
-                     ... | tri< a ¬b ¬c = ⊥-elim (p a)
-                     ... | tri≈ ¬a b ¬c = ?
-                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c )
-                     csupf2 | case1 p with trio< (supf0 px) px           --  ¬ (supf0 px ≡ px )
-                     ... | tri< sf0px<px ¬b ¬c = ? where
-                           cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px)
-                           cs10 = ZChain.csupf zc sf0px<px
-                     ... | tri≈ ¬a b ¬c = ⊥-elim (p b)
-                     ... | tri> ¬a ¬b px<sf0px = ? where
-                           cs11 : px o< z1 →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                           cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) 
-                              (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 )))  sfpx≤sp1 ) sz1<x) ⟫ )
-                           cs12 : z1 o≤ px →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                           cs12 = ?
+                 csupf1 : {z1 : Ordinal } → supf1 z1 o< supf1 x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
+                 csupf1 {z1} sz<sx = ⟪ ? , ch-is-sup (supf1 z1) ? ? (init ? ? ) ⟫
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
@@ -1594,15 +1400,11 @@
           msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
           c : Ordinal
           c = MinSUP.sup msp1
-          mc = c
-          mc<A : mc o< & A
-          mc<A =  ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫
-          c=mc : c ≡ mc
-          c=mc = refl
-          z20 : mc << cf nmx mc
-          z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) )
-          asc : odef A (supf mc)
+          c<A : c o< & A
+          c<A =  ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫
+          asc : odef A (supf c)
           asc = ZChain.asupf zc
+
           spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )
           spd = ysup (cf nmx)  (cf-is-≤-monotonic nmx) asc
           d = MinSUP.sup spd
@@ -1636,152 +1438,14 @@
                     ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  )
                     ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt)
 
-          fsc<<d : {mc z : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
-             → (fc : FClosure A (cf nmx) (supf mc) z) → z << MinSUP.sup spd
-          fsc<<d {mc} {z} asc spd fc = z25 where
-                d1 :  Ordinal
-                d1 = MinSUP.sup spd -- supf d1 ≡ d
-                z24 : (z ≡ d1) ∨ ( z << d1 )
-                z24 = MinSUP.x≤sup spd fc
-                --
-                --   f ( f .. ( supf mc ) <= d1
-                --   f d1 <= d1
-                --
-                z25 : z << d1
-                z25 with z24
-                ... | case2 lt = lt
-                ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
-                    --  supf mc ≡ d1
-                    z32 : ((cf nmx z) ≡ d1) ∨ ( (cf nmx z) << d1 )
-                    z32 = MinSUP.x≤sup spd (fsuc _ fc)
-                    z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                    z29  with z32
-                    ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  )
-                    ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt)
-
-          smc<<d : supf mc << d
-          smc<<d = sc<<d asc spd
-
-          sz<<c : {z : Ordinal } → z o< & A → supf z <= mc
-          sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
-
-          sc=c : supf mc ≡ mc
-          sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
-              not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc
-              not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where
-                   z30 : * mc < * (cf nmx mc)
-                   z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
-                   z31 : ( * (cf nmx mc)  ≡  * mc ) ∨ ( * (cf nmx mc) < * mc )
-                   z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k →  odef (ZChain.chain zc) (cf nmx k)) (sym x=fy)
-                       ⟪ proj2  (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc))  ⟫ ))
-              not-hasprev record { ax = ax ; y = y ; ay =   ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where
-                   z30 : * mc < * (cf nmx mc)
-                   z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
-                   z31 : ( supf mc ≡  mc ) ∨ ( * (supf mc) < * mc )
-                   z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
-                   z32 : * (supf mc) < * (cf nmx (cf nmx y))
-                   z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
-                   z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
-                   z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
-              is-sup :  IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc)  (MinSUP.asm msp1)
-              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) }
-
+          z11 : odef (ZChain.chain zc) d
+          z11 = ZChain1.is-max (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) {& s} ? ? ? ? ? where
 
-          not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d
-          not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where
-                z30 : * d < * (cf nmx d)
-                z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))
-                z32 : ( cf nmx (cf nmx y)  ≡  supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) )
-                z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc))
-                z31 : ( * (cf nmx d)  ≡  * d ) ∨ ( * (cf nmx d) < * d )
-                z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) ))
-          not-hasprev record { ax = ax ; y = y ; ay =   ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where
-                z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
-                z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p
-                z48 : supf mc << d
-                z48 = sc<<d {mc} asc spd
-                z53 : supf u o< supf (& A)
-                z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
-                z52 : ( u ≡ mc ) ∨  ( u << mc )
-                z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc)
-                        , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
-                z51 : supf u o≤ supf mc
-                z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where
-                    z56 : u ≡ mc → supf u ≡  supf mc
-                    z56 eq = cong supf eq
-                    z57 : u << mc → supf u o≤ supf mc
-                    z57 lt = ZChain.supf-<= zc (case2 z58) where
-                        z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
-                        z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt
-                z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
-                z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc  _ fc ))
-                z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) )
-                z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc  _ fc ))
-                z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
-                    → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1
-                    →  * (cf nmx (cf nmx y)) < * d1
-                z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq))  smc<d
-                z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d
-                z30 : * d < * (cf nmx d)
-                z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))
-                z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
-                z46 = or (osuc-≡< z51) z55 z54 where
-                   z55  : supf u ≡  supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
-                   z55 eq = <=to≤  (MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j (cf nmx k) ) eq (sym x=fy ) (fsuc _ (fsuc _ fc)) ) )
-                   z54  : supf u o< supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
-                   z54 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 ))
-                -- z46 with osuc-≡< z51
-                -- ... | case1 eq =  MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup1) eq) refl fc )
-                -- ... | case2 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 ))
-
-          is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d)  (MinSUP.asm spd)
-          is-sup = record { x≤sup = z22 } where
-                z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
-                z23 lt = MinSUP.x≤sup spd lt
-                z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
-                   (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
-                z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where
-                    z32 : ( a  ≡  supf mc ) ∨ ( * a < * (supf mc) )
-                    z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc
-                z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc)
-                       z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where
-                    z53 : supf u o< supf (& A)
-                    z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
-                    z52 : ( u ≡ mc ) ∨  ( u << mc )
-                    z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc)
-                           , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
-                    z56 : u ≡ mc → supf u ≡  supf mc
-                    z56 eq = cong supf eq
-                    z57 : u << mc → supf u o≤ supf mc
-                    z57 lt = ZChain.supf-<= zc (case2 z58) where
-                        z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
-                        z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt
-                    z51 : supf u o≤ supf mc
-                    z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57
-                    z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d )
-                    z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A
-                        (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1))  u<smc)  fc ) smc<<d )
-                    z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d )
-                    z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) )
-                    -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
-                    --     supf u o< supf c → order
-
-          sd=d : supf d ≡ d
-          sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
-
-          sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
-          sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
-          ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
-          ... | case2 lt = lt
-
-          sms<sa : supf mc o< supf (& A)
-          sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
-          ... | case2 lt = lt
-          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) )
-              ( ZChain.supf-mono zc (o<→≤ d<A ))))
+          z10 : supf d o≤ supf (& A)
+          z10 = ?
 
           ss<sa : supf c o< supf (& A)
-          ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa
+          ss<sa = ?
 
      zorn00 : Maximal A
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM