# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661121558 -32400
# Node ID 507f6582c31da4790879fb9918e039f79082f597
# Parent  4822758b8bf8ab19591bc6de0ff6718b31372352
...

diff -r 4822758b8bf8 -r 507f6582c31d src/OD.agda
--- a/src/OD.agda	Fri Aug 19 10:08:14 2022 +0900
+++ b/src/OD.agda	Mon Aug 22 07:39:18 2022 +0900
@@ -120,7 +120,7 @@
 
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
-¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
+¬OD-order & * c<→o< = o≤> <-osuc (c<→o< {Ords} OneObj )
 
 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup
 ¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥
diff -r 4822758b8bf8 -r 507f6582c31d src/OrdUtil.agda
--- a/src/OrdUtil.agda	Fri Aug 19 10:08:14 2022 +0900
+++ b/src/OrdUtil.agda	Mon Aug 22 07:39:18 2022 +0900
@@ -35,10 +35,10 @@
 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
 
-osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
-osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
-osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
-osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
+o≤> :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
+o≤> {x} {y} y<ox x<y with osuc-≡< y<ox
+o≤> {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
+o≤> {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
 
 open _∧_
@@ -207,7 +207,7 @@
 o≤? x y with trio< x y
 ... | tri< a ¬b ¬c = yes (ordtrans a <-osuc)
 ... | tri≈ ¬a b ¬c = yes (o≤-refl0 b)
-... | tri> ¬a ¬b c = no (λ n → osuc-< n c )
+... | tri> ¬a ¬b c = no (λ n → o≤> n c )
 
 o¬≤→< : {x z : Ordinal} →  ¬ (x o< osuc z) → z o< x
 o¬≤→< {x} {z} not with trio< z x
diff -r 4822758b8bf8 -r 507f6582c31d src/zorn.agda
--- a/src/zorn.agda	Fri Aug 19 10:08:14 2022 +0900
+++ b/src/zorn.agda	Mon Aug 22 07:39:18 2022 +0900
@@ -304,16 +304,14 @@
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
 
-   order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   order {b} {s} {z1} b<z ss<sb fc = zc04 where
-      zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-      zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
+   csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+   csupf-fc {b} {s} {z1} b≤<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
             s<b : s o< b
             s<b = supf-inject ss<sb
-            s<z : s o< z
-            s<z = ordtrans s<b b<z
+            s≤<z : s o≤ z
+            s≤<z = ordtrans s<b b≤<z
             zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
-            zc04 = csupf (o<→≤ s<z )
+            zc04 = csupf s≤<z 
             zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
             zc05 with zc04
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
@@ -330,13 +328,15 @@
                     ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb )
                     ... | case2 lt =  o<→≤ (supf-inject lt )
                 ... | case2 lt =  o<→≤ (ordtrans (supf-inject lt) s<b) 
-      zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
+   csupf-fc {b} {s} {z1} b<z ss<sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
-            zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
+            zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss<sb fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
+   order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+   order {b} {s} {z1} b<z ss<sb fc = zc04 where
       zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
-      zc00 = SUP.x<sup (sup  b<z) (zc01 fc )
+      zc00 = SUP.x<sup (sup  b<z) (csupf-fc (o<→≤ b<z) ss<sb fc )
       zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
       zc04 with zc00
       ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  b<z)  ) (cong (&) eq) )
@@ -669,7 +669,7 @@
           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
           pchain : HOD
-          pchain  = UnionCF A f mf ay (ZChain.supf zc) x
+          pchain  = UnionCF A f mf ay (ZChain.supf zc) px
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
@@ -690,14 +690,14 @@
 
           supf0 = ZChain.supf zc
 
-          sup1 : SUP A (UnionCF A f mf ay supf0 x)
+          sup1 : SUP A (UnionCF A f mf ay supf0 px)
           sup1 = supP pchain pchain⊆A ptotal
           sp1 = & (SUP.sup sup1 )
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z px
           ... | tri< a ¬b ¬c = ZChain.supf zc z
-          ... | tri≈ ¬a b ¬c = sp1 -- ZChain.supf zc z
-          ... | tri> ¬a ¬b c = sp1 -- ZChain.supf zc px
+          ... | tri≈ ¬a b ¬c = sp1 
+          ... | tri> ¬a ¬b c = sp1 
 
           pchain1 : HOD
           pchain1  = UnionCF A f mf ay supf1 x
@@ -717,6 +717,34 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
 
+          zc64 : {z : Ordinal } → z o< px → odef (UnionCF A f mf ay supf0 px) (supf0 z)
+          zc64 {z} z<px = chain-mono f mf ay supf0 zc72 zc70  where
+               zc70 : odef (UnionCF A f mf ay supf0 (supf0 z) ) (supf0 z)
+               zc70 = ZChain.csupf zc (o<→≤ z<px )
+               zc71 : supf0 z o≤ supf0 px
+               zc71 = ZChain.supf-mono zc (o<→≤ z<px )
+               zc72 : supf0 z o≤ px
+               zc72 = ?
+               zc73 : odef (UnionCF A f mf ay supf0 px ) (supf0 z)
+               zc73 = subst (λ k → odef (UnionCF A f mf ay supf0 px ) k ) &iso ( ZChain.csupf-fc zc  o≤-refl  ? (init (proj1 zc70) refl) )
+
+          supf1<sp1 : {z : Ordinal } → supf1 z o≤ sp1
+          supf1<sp1 {z} with trio< z px | inspect supf1 z
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = o≤-refl 
+          ... | tri> ¬a ¬b c | record { eq = eq1 } = o≤-refl
+          ... | tri< a ¬b ¬c | record { eq = eq1 } with trio< (supf1 z) sp1
+          ... | tri< a₁ ¬b₁ ¬c₁ = subst (λ k → k o≤ sp1) eq1 (o<→≤ a₁)
+          ... | tri≈ ¬a b ¬c₁ = o≤-refl0 (trans (sym eq1) b )
+          ... | tri> ¬a ¬b₁ c = ? where
+              zc65 : sp1 o< ZChain.supf zc z
+              zc65 = subst (λ k → sp1 o< k ) eq1 c
+              zc66 :  ( * (ZChain.supf zc z) ≡ * sp1) ∨  (ZChain.supf zc z <<  sp1) 
+              zc66 = subst₂ (λ j k → ( j ≡   k) ∨ ( j  < k ) ) refl (sym *iso)  zc68 where
+                 zc68 : ( *( ZChain.supf zc z) ≡ SUP.sup sup1  ) ∨ ( * (ZChain.supf zc z) < SUP.sup sup1  )
+                 zc68 =  SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 px) k ) (sym &iso) (zc64 a) )
+              zc67 : ZChain.supf zc sp1 ≡ sp1
+              zc67 = ?
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
@@ -732,25 +760,27 @@
               zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w
               zc60 (init asp refl) with trio< u1 px | inspect supf1 u1
               ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
                   fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
-                  order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
+                  order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
                     (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
                   order {s} {z2} s<u1 fc with trio< s px 
-                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
-                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? ? )
-                  ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
+                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup zc61 fc ) where
+                      zc61 : supf0 s o< supf0 u1
+                      zc61 = subst (λ k → supf0 s o< k ) eq1 s<u1
+                  ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> supf1<sp1 s<u1 )
+                  ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s {!!} ))  --  px o< s < u1 < px
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 ?   } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? )  ⟫ where
+                record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 {!!}   } (init (subst (λ k → odef A k ) (sym eq1) {!!} ) {!!} )  ⟫ where
                   fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
-                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ? -- ( ChainP.fcy<sup u1-is-sup fc )
-                  order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
+                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) {!!} -- ( ChainP.fcy<sup u1-is-sup fc )
+                  order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
                     (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
                   order {s} {z2} s<u1 fc with trio< s px 
-                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
-                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
-                  ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
+                  ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) {!!}
+                  ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) {!!} -- ( ChainP.order u1-is-sup s<u1 fc )
+                  ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b {!!} ) ))  --  px o< s < u1 = px
               ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x (o<→≤ z0<px))
               ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
               ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
@@ -758,8 +788,8 @@
               ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
               ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
           no-extension : ¬ xSUP → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = ?
-               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = ?
+          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = {!!}
+               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = {!!}
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
                  UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o< x → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 
                  UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
@@ -767,24 +797,24 @@
                       zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w
                       zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1
                       ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                        record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init asp refl )  ⟫ where
+                        record { fcy<sup = fcy<sup ; order = {!!} ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init asp refl )  ⟫ where
                           fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
                           fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
                           order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
                             (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
                           order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-                          ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) ? ))
+                          ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) {!!} ))
                           ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
                       ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                        record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans (sym ? ) (ChainP.supu=u u1-is-sup)   } (init ? ? )  ⟫ where
+                        record { fcy<sup = fcy<sup ; order = {!!} ; supu=u = trans (sym {!!} ) (ChainP.supu=u u1-is-sup)   } (init {!!} {!!} )  ⟫ where
                           fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
-                          fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
+                          fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) {!!} ( ChainP.fcy<sup u1-is-sup fc )
                           order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
                             (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
                           order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-                          ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ?( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) ? ))
+                          ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) {!!}( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                          ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) {!!} ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) {!!} ))
                           ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
                       ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px
                       ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) )
@@ -802,13 +832,13 @@
                  ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z<x  ) ( ZChain.sup zc  a ) 
                  ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
                      zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x  lt )
+                     zc61 {w} lt = ? -- SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x  lt )
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl  a lt) } 
-                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
+                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
                  ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -816,16 +846,16 @@
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                      zcsup : xSUP
                      zcsup with zc30
-                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) ? lt) } } 
+                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) {!!} lt) } } 
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b<x with trio< b px | inspect supf1 b
-                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ?
-                 ... | tri≈ ¬a refl ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
-                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? --  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
+                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a {!!}
+                 ... | tri≈ ¬a refl ¬c | _ = {!!} -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
+                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = {!!} --  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
                  sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))
                  sis {z} z<x with trio< z px
                  ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a
-                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x  ⟫ )
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -835,7 +865,7 @@
           ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; sup=u = {!!} ; supf-mono = ?
+                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
                    ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supx : SUP A (UnionCF A f mf ay supf0 x)
              supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
@@ -933,8 +963,8 @@
 
           no-extension : ¬ xSUP → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
-               ; sup = sup ; supf-is-sup = sis ; supf-mono = ?
-               ; csupf = ? ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
+               ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!}
+               ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x 
@@ -973,9 +1003,9 @@
                      zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
                      zc9 = {!!}
                      zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
-                     zc8 = ? -- ZChain.csupf  (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc )
+                     zc8 = {!!} -- ZChain.csupf  (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc )
                  ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z ? )) 
+                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z {!!} )) 
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
@@ -985,7 +1015,7 @@
           ... | case1 pr = no-extension {!!} 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = supf1  ; sup=u = {!!} 
-               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = ?
+               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}
                ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention