# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660870347 -32400
# Node ID 802d70b7ea0147795ebe493c2fbe3fe6595b0f3b
# Parent  685f7ae1b821a7ea2b5e986d3e4efc8ca3165417
csupf fix

diff -r 685f7ae1b821 -r 802d70b7ea01 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 19 09:30:32 2022 +0900
+++ b/src/zorn.agda	Fri Aug 19 09:52:27 2022 +0900
@@ -251,7 +251,8 @@
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
-      order    : {s z1 : Ordinal} → (lt : s o< u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+      order    : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+      supu=u   : supf u ≡ u
 
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
@@ -286,10 +287,7 @@
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
-      --  supf b ≡ b → csupf0 → csupf
-   csupf0 : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b) ) (supf b) 
-   csupf0 {b}  b≤z = ?
+      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y 
    supf-inject {x} {y} sx<sy with trio< x y
    ... | tri< a ¬b ¬c = a
@@ -306,41 +304,32 @@
    ... | 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 )
 
-   -- supf s o< b
-   order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   order {b} {s} {z1} b<z s<b fc = zc04 where
+   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) zc03  where
+      zc01  (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
             zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
-            zc04 = ?
+            zc04 = csupf (o<→≤ s<z )
             zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
             zc05 with zc04
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where
+            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u≤x ) is-sup fc ⟫ where
                 zc06 : supf u ≡ u
-                zc06 = sup=u ? ? ?
-                zc09 : u o≤ supf s  → ( u o≤ b ) ∨ ( supf u ≡ supf b )
+                zc06 = ChainP.supu=u is-sup
+                zc09 : u o≤ supf s  →  u o≤ b 
                 zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s)
                 ... | case1 su=ss = zc08 where
                     zc07 : supf u o≤ supf b   
                     zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono  (o<→≤ s<b)  )
-                    zc08 : ( u o≤ b ) ∨ ( supf u ≡ supf b )
+                    zc08 :  u o≤ b 
                     zc08 with osuc-≡< zc07
-                    ... | case1 su=sb = case2 su=sb
-                    ... | case2 lt = case1 ( o<→≤ (supf-inject lt )) 
-                ... | case2 lt = case1 ( o<→≤ (ordtrans (supf-inject lt) s<b) )
-                zc10 :  odef (UnionCF A f mf ay supf b)  (supf s)
-                zc10 with zc09 u≤x
-                ... | case1 lt = ⟪ as , ch-is-sup u lt is-sup fc ⟫ 
-                ... | case2 eq = ⟪ as , ch-is-sup b ? record { fcy<sup = ? ; order = ? } (init ? ? )  ⟫  where
-                    zc11 : supf (supf s) ≡  supf s
-                    zc11 = ?
-            zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
-            zc03 with csupf (o<→≤ s<z) 
-            ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ 
+                    ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans ? 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
             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  )
@@ -404,7 +393,7 @@
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
-     ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ fca 
+     ... | tri< a₁ ¬b ¬c with ChainP.order supb  ? fca 
      ... | case1 eq with s≤fc (supf ub) f mf fcb 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -421,7 +410,7 @@
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c 
          = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa c fcb 
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa ? fcb 
      ... | case1 eq with s≤fc (supf ua) f mf fca 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -550,11 +539,12 @@
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz )  }  )
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
-              m09 : {s z1 : Ordinal} → s o< b 
+              m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz    
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record {  fcy<sup = m08  ; order = m09 }
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } }  
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -569,14 +559,15 @@
               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
               m07 {z} fc = ZChain.fcy<sup zc  m09 fc
-              m08 : {s z1 : Ordinal} → s o< b 
+              m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab (o<→≤  m09)
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} )   -- ZChain on x
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record { fcy<sup = m07 ;  order = m08 }
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab (o<→≤  m09)
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} } 
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -741,17 +732,17 @@
               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 = order  } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                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
                   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 →
                     (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 ? )
+                  ... | 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 | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                record { fcy<sup = fcy<sup ; order = order } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? )  ⟫ where
+                record { fcy<sup = fcy<sup ; 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 →
@@ -768,7 +759,7 @@
               ... | ⟪ 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
-               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
+               ; 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 ⟫ 
@@ -776,24 +767,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 = order } (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 s<u1 (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 s<u1 (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 = order } (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 )
                           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 s<u1 (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 s<u1 (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) )
@@ -828,7 +819,7 @@
                      ... | 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 ( ZChain.csupf zc (o<→≤ a)  )
+                 ... | 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))
@@ -844,7 +835,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 = csupf ; sup=u = {!!} 
+                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; sup=u = {!!} 
                    ;  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 = {!!} }
@@ -943,7 +934,7 @@
           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
-               ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
+               ; 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 
@@ -982,7 +973,7 @@
                      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 ? ))