# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669885244 -32400
# Node ID 84881efe649b45e8612e047709e3cc18262bdd41
# Parent  2da8dcbb0825b9d1c34865c10c8f7546744c024d
...

diff -r 2da8dcbb0825 -r 84881efe649b src/zorn.agda
--- a/src/zorn.agda	Thu Dec 01 11:31:15 2022 +0900
+++ b/src/zorn.agda	Thu Dec 01 18:00:44 2022 +0900
@@ -514,7 +514,12 @@
                  supfa x ∎ ) a ) where 
                     open o≤-Reasoning O
                     z53 : {z : Ordinal } →  odef (UnionCF A f ay (ZChain.supf zb) x) z →  odef (UnionCF A f ay (ZChain.supf za) x) z
-                    z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫ 
+                    z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                    z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ⟪ as , ch-is-sup u u<x (trans ua=ub su=u) z55 ⟫ where
+                        ua=ub : supfa u ≡ supfb u
+                        ua=ub = prev u u<x (ordtrans u<x x≤xa )
+                        z55 : FClosure A f (ZChain.supf za u) z
+                        z55 = subst (λ k → FClosure A f k z ) (sym ua=ub) fc
            ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
                begin
                  supfa x  ≡⟨ sax=spa ⟩
@@ -523,17 +528,12 @@
                  supfb x ∎ ) c ) where 
                     open o≤-Reasoning O
                     z53 : {z : Ordinal } →  odef (UnionCF A f ay (ZChain.supf za) x) z →  odef (UnionCF A f ay (ZChain.supf zb) x) z
-                    z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫ 
-
-UChain-eq : { A : HOD }    { f : Ordinal → Ordinal }  {mf : ≤-monotonic-f A f}
-        {z y : Ordinal} {ay : odef A y}  { supf0 supf1 : Ordinal → Ordinal }
-        → (seq : {x : Ordinal } →  x o<  z  → supf0 x ≡ supf1 x )
-        → UnionCF A f ay supf0 z ≡ UnionCF A f ay supf1 z
-UChain-eq {A} {f} {mf} {z} {y} {ay} {supf0} {supf1} seq = ==→o≡  record { eq← = ueq← ; eq→ = ueq→ } where
-      ueq← :  {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ?
-      ueq← {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ 
-      ueq→  : {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ?
-      ueq→ {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ 
+                    z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                    z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ =  ⟪ as , ch-is-sup u u<x (trans ub=ua su=u) z55  ⟫ where
+                        ub=ua : supfb u ≡ supfa u
+                        ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa ))
+                        z55 : FClosure A f (ZChain.supf zb u) z
+                        z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
 
 Zorn-lemma : { A : HOD }
     → o∅ o< & A
@@ -607,9 +607,9 @@
              S = supP B  B⊆A total
              s1 = & (SUP.sup S)
              m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 )
-             m05 {w} bw with SUP.x≤sup S ? -- ? (subst (λ k → odef B k) (sym &iso) bw )
-             ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl ?) -- (cong (&) eq) )
-             ... | case2 lt = case2 ? -- ( subst (λ k → _ < k ) (sym *iso) lt )
+             m05 {w} bw with SUP.x≤sup S bw 
+             ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq)) 
+             ... | case2 lt = case2 lt 
          m02 : MinSUP A B
          m02 = dont-or (m00 (& A)) m03
 
@@ -652,7 +652,10 @@
             → HasPrev A (UnionCF A f ay (ZChain.supf zc) x) f b
             → * a < * b → odef (UnionCF A f ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev
-        ... | ⟪ ab0 , cp ⟫ = ⟪ ab , ? ⟫
+        ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
+        ... | ⟪ ab0 , ch-is-sup u u<x su=u fc ⟫ = ⟪ ab , subst (λ k → UChain ay x k )
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x su=u (fsuc _ fc))  ⟫
+
 
         supf = ZChain.supf zc
 
@@ -662,7 +665,7 @@
                px = Oprev.oprev op
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a →
                   b o< x → (ab : odef A b) →
-                  HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) ? →
+                  HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) b →
                   * a < * b → odef (UnionCF A f ay supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
@@ -674,7 +677,7 @@
                   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 } )
                   m05 : ZChain.supf zc b ≡ b
-                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
@@ -690,7 +693,7 @@
                           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 } )
                           m05 : ZChain.supf zc b ≡ b
-                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
@@ -703,8 +706,8 @@
                   * a < * b → odef (UnionCF A f ay supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc ? )
-               ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ?  ⟫
+               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc (ordtrans b<x x≤A) )
+               ... | 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 with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
                   m09 : b o< & A
@@ -802,28 +805,22 @@
           --
 
           pchainpx : HOD
-          pchainpx = record { od = record { def = λ z →  (odef A z ∧ ? )
+          pchainpx = record { od = record { def = λ z →  (odef A z  ∧ UChain  ay px z )
                 ∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
-               zc00 : {z : Ordinal } → (odef A z ∧ ? ) ∨ FClosure A f (supf0 px) z → z o< & A
+               zc00 : {z : Ordinal } → (odef A z ∧ UChain ay px z ) ∨ FClosure A f (supf0 px) z → z o< & A
                zc00 {z} (case1 lt) = z07 lt
                zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc )
 
-          zc02 : { a b : Ordinal } → odef A a ∧ ? → FClosure A f (supf0 px) b → a ≤ b
+          zc02 : { a b : Ordinal } → odef A a ∧ UChain ay px a → FClosure A f (supf0 px) b → a ≤ b
           zc02 {a} {b} ca fb = zc05 fb where
-             zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px
-             zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl
              zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a ≤ b
              zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
-             ... | case1 eq = subst (λ k → a ≤ k ) (subst₂ (λ j k → j ≡ k) &iso &iso ?) (zc05 fb)
+             ... | case1 eq = subst (λ k → a ≤ k ) eq (zc05 fb)
              ... | case2 lt = ≤-ftrans (zc05 fb) (case2 lt)
-             zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl)
-                (subst (λ k → odef A k ∧ ?) (sym &iso) ca )
-             ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
-             ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt )
+             zc05 (init b1 refl) = MinSUP.x≤sup (ZChain.minsup zc o≤-refl) ca
 
           ptotal : IsTotalOrderSet pchainpx
-          ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso
-                   ?
+          ptotal (case1 a) (case1 b) =  ZChain.f-total zc a b
           ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
           ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
                eq1 : a0 ≡ b0
@@ -848,17 +845,23 @@
           sup1 = minsupP pchainpx pcha ptotal
           sp1 = MinSUP.sup sup1
 
-          sfpx≤sp1 : supf0 px ≤ sp1
-          sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
-
           --
           --     supf0 px o≤ sp1
           --
 
+          sfpx≤sp1 : supf0 px ≤ sp1
+          sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
+
+          m13 : supf0 px o≤ sp1
+          m13 = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1)  m14 where
+             m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
+             m14 {z} ⟪ as , ch-init fc ⟫ = ?
+             m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ? 
+
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x sp1
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs  }  where
+              ; supfmax = ? ; is-minsup = ? ;  cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px
@@ -937,7 +940,7 @@
                       --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
                       z50 : odef (UnionCF A f ay supf1 b) w
                       z50 with osuc-≡< px≤sa
-                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ?  ⟫ where
+                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , cp  ⟫ where
                           sa≤px : supf0 a o≤ px
                           sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
                           spx=sa : supf0 px ≡ supf0 a
@@ -955,45 +958,14 @@
                                 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
                                 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ 
                                 supf1 (supf0 px) ∎ where open ≡-Reasoning
-                          m : MinSUP A (UnionCF A f ay supf0 px)
-                          m = ZChain.minsup zc o≤-refl
-                          m=spx : MinSUP.sup m ≡ supf1 (supf0 px)
-                          m=spx = begin 
-                                MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl)  ⟩ 
-                                supf0 px ≡⟨ cong supf0 px=sa  ⟩ 
-                                supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩
-                                supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa)  ⟩
-                                supf1 (supf0 px)  ∎  where open ≡-Reasoning 
                           z53 : supf1 (supf0 px) ≡ supf0 px
                           z53 = begin
                                 supf1 (supf0 px)  ≡⟨ cong supf1 spx=sa ⟩ 
                                 supf1 (supf0 a)  ≡⟨ sf1=sf0 sa≤px ⟩ 
                                 supf0 (supf0 a)  ≡⟨ sym ( cong supf0 px=sa ) ⟩ 
                                 supf0 px  ∎  where open ≡-Reasoning 
-                          cp : ?
-                          cp = ? where
-                             uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f ay supf0 px) z1
-                             uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) 
-                                     (sf1=sf0 (o<→≤ s<px))  fc ) where
-                                s<spx : s o< supf0 px
-                                s<spx = supf-inject0 supf1-mono ss<sp
-                                s<px : s o< px
-                                s<px = osucprev ( begin
-                                     osuc s  ≤⟨  osucc s<spx   ⟩  
-                                     supf0 px  ≡⟨ spx=sa  ⟩ 
-                                     supf0 a ≡⟨ sym px=sa  ⟩ 
-                                     px ∎ )   where open o≤-Reasoning O
-                                ss<px : supf0 s o< px
-                                ss<px = osucprev ( begin
-                                     osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 (o<→≤ s<px)))  ⟩ 
-                                     osuc (supf1 s)  ≤⟨ osucc ss<sp  ⟩ 
-                                     supf1 (supf0 px)  ≡⟨ sym z52  ⟩ 
-                                     supf1 a  ≡⟨ sf1=sf0 a≤px  ⟩ 
-                                     supf0 a  ≡⟨ sym px=sa  ⟩ 
-                                     px ∎ )   where open o≤-Reasoning O
-                             order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) →
-                                    FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px))
-                             order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m (uz s<u fc) )
+                          cp : UChain ay b w
+                          cp = ch-is-sup (supf0 px) z51 z53 (subst (λ k → FClosure A f k w) z52 fc) 
                       ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫  ) where
                           z53  : supf1 a o< x
                           z53  = ordtrans<-≤ sa<b b≤x
@@ -1002,9 +974,19 @@
                       z50 : odef (UnionCF A f ay supf1 b) w
                       z50 with osuc-≡< b≤x
                       ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc  
-                      ... | ⟪ az , cp ⟫ = ⟪ az , ?  ⟫  -- u o< px → u o< b ?
+                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                      ... | ⟪ az , ch-is-sup u u<b su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc u≤px )  ⟫ where
+                           u≤px : u o≤ px
+                           u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b b≤x )
+                           u<x : u o< x
+                           u<x = ordtrans<-≤ u<b b≤x 
                       z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc  
-                      ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫  -- u o< px → u o< b ?
+                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                      ... | ⟪ az , ch-is-sup u u<px su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
+                           u<b : u o< b
+                           u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc )
+                           u<x : u o< x
+                           u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc )
                  ... | tri≈ ¬a a=px ¬c = csupf1 where
                       -- a ≡ px , b ≡ x, sp o≤ x 
                       px<b : px o< b
@@ -1020,7 +1002,7 @@
                       z53 = A∋fc {A} _ f mf fc
                       csupf1 : odef (UnionCF A f ay supf1 b) w
                       csupf1 with trio< (supf0 px) x
-                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ? ⟫  where
+                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫  where
                           spx = supf0 px
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
@@ -1028,39 +1010,26 @@
                           z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl (zc-b<x _ sfpx<x ) )
                           fc1 : FClosure A f (supf1 spx) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
-                          order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
-                          order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
-                                   (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
-                                   (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                       spx≤px ss0<spx (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
-                                          ss0<spx : supf0 s o< spx
-                                          ss0<spx = osucprev ( begin
-                                            osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 ( begin
-                                               s <⟨ supf-inject0 supf1-mono ss<spx ⟩
-                                               supf0 px  ≤⟨ spx≤px ⟩
-                                               px ∎ ) )) ⟩
-                                            osuc (supf1 s)  ≤⟨ osucc ss<spx ⟩
-                                            supf1 spx  ≡⟨ sf1=sf0 spx≤px  ⟩
-                                            supf0 spx  ≤⟨ ZChain.supf-mono zc spx≤px ⟩
-                                            supf0 px  ∎  ) where open o≤-Reasoning O
                       ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
                           -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
                           m12 : supf0 px ≡ sp1
-                          m12 with osuc-≡< ? -- sfpx≤sp1
+                          m12 with osuc-≡< m13
                           ... | case1 eq = eq
-                          ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) -- supf0 px o< sp1 , x o< sp1
+                          ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) 
                           m10 : f (supf0 px) ≡ supf0 px
                           m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where
                               m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1)
                               m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc)  
-                      ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans ? sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
+                      ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
 
                  zc11 : {z : Ordinal} → odef (UnionCF A f ay supf1 x) z → odef pchainpx z
-                 zc11 {z} ⟪ az , cp ⟫ = zc21 ? where
-                    zc21 : {z1 : Ordinal } → FClosure A f (supf1 ?) z1 → odef pchainpx z1
+                 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
+                 zc11 {z} ⟪ az , ch-is-sup u u<x su=u 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 , cp  ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ? ⟫
+                    ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
+                    ... | case1 ⟪ ua1 ,  ch-is-sup u u<x su=u fc₁   ⟫ = case1 ⟪ proj2 ( mf _ ua1)  ,  ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫
                     ... | case2 fc = case2 (fsuc _ fc)
                     zc21 (init asp refl ) = ?