# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671161117 -32400
# Node ID 2624f8a9f6edae2756b55d0dd01ec6b617a14673
# Parent  faa512b2425ca6d50468b40d4106f9fc9b392c9a
...

diff -r faa512b2425c -r 2624f8a9f6ed src/zorn.agda
--- a/src/zorn.agda	Fri Dec 16 10:08:05 2022 +0900
+++ b/src/zorn.agda	Fri Dec 16 12:25:17 2022 +0900
@@ -283,13 +283,13 @@
 
 -- Union of chain lower than x
 
-data IChain  {A : HOD}  { f : Ordinal → Ordinal } {y : Ordinal } (ay : odef A y ) 
+data IChain  {A : HOD}  { f : Ordinal → Ordinal } {y : Ordinal } (ay : odef A y )
                {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) : (z : Ordinal ) → Set n where
     ic-init : {z : Ordinal } (fc : FClosure A f y z) → IChain ay supfz z
     ic-isup : {z : Ordinal} (i : Ordinal) (i<x : i o< x) (s<x : supfz i<x o≤ i ) (fc : FClosure A f (supfz i<x) z) → IChain ay supfz z
 
 UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal)  → HOD
-UnionIC A f ay supfz 
+UnionIC A f ay supfz
    = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} ay supfz z } ;
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
@@ -440,30 +440,30 @@
    f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
       subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
 
-   supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b 
+   supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
    supf-mono< {a} {b} b≤z sa<sb  with order {a} {b} b≤z sa<sb (init asupf refl)
    ... | case2 lt = lt
-   ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) 
+   ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
 
-   supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b 
+   supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
    supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b)
    ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
-             IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) 
+             IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
    ... | tri≈ ¬a b ¬c = b
    ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
-             IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) 
+             IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
 
-   union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b 
+   union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
    union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
           z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
-          z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+          z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
           z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
-              u<b : u o< b  
+              u<b : u o< b
               u<b = ordtrans u<a (supf-inject sa<sb )
           z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w
-          z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+          z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
           z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
-              u<a : u o< a 
+              u<a : u o< a
               u<a = supf-inject ( osucprev (begin
                  osuc (supf u)  ≡⟨ cong osuc su=u ⟩
                  osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
@@ -481,7 +481,7 @@
                  z47 : b o≤ supf b
                  z47 = zo≤sz b≤z
            ... | tri≈ ¬a b ¬c = b
-           ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) 
+           ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb )
 
    supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
    supf-idem {b} b≤z sfb≤x = z52 where
@@ -491,20 +491,20 @@
                u<b : u o< b
                u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
        z52 : supf (supf b) ≡ supf b
-       z52 = sup=u asupf sfb≤x  record { ax = asupf  ; x≤sup = z54  } 
+       z52 = sup=u asupf sfb≤x  record { ax = asupf  ; x≤sup = z54  }
 
-   x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x 
+   x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x
    x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
    ... | case2 le = le
-   ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where 
+   ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where
          z46 : odef (UnionCF A f ay supf x) (f (supf x))
          z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf  z47 )) ⟫ where
              z47 : supf (supf x) ≡ supf x
              z47 = supf-idem x≤z  sx≤z
          z45 : f (supf x) ≤ supf x
-         z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 
+         z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
 
-   order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b 
+   order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b
    order0 {a} {b} {w} b≤z sa<sb sa≤z fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where
          sa<b : supf a o< b
          sa<b with x<y∨y≤x (supf a) b
@@ -717,7 +717,7 @@
                   b<A : b o< & A
                   b<A = z09 ab
                   m05 : ZChain.supf zc b ≡ b
-                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  } 
+                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc 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
@@ -733,7 +733,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 { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
                           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
@@ -753,7 +753,7 @@
                   m09 : b o< & A
                   m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
                   m05 : ZChain.supf zc b ≡ b
-                  m05 = ZChain.sup=u zc ab (o<→≤  m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } 
+                  m05 = ZChain.sup=u zc ab (o<→≤  m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt }
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc 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
@@ -765,7 +765,7 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } 
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz }
                           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
@@ -895,8 +895,8 @@
              m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz)
 
           zc41 : ZChain A f mf< ay x
-          zc41 =  record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order 
-              ; 0<supfz = 0<supfz 
+          zc41 =  record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
+              ; 0<supfz = 0<supfz
               ; zo≤sz = zo≤sz ;  is-minsup = is-minsup ;  cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
@@ -1080,7 +1080,7 @@
                     zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z ))  ( MinSUP.as sup1 )
                     z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
                     z23 {w} uz  = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (
-                         zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ))) 
+                         zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz )))
                     z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )
                         → supf1 z o≤ s
                     z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where
@@ -1123,25 +1123,25 @@
                                 u≤px : u o≤ px
                                 u≤px = ordtrans u<x z≤px
 
-                 supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b 
+                 supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
                  supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
                  ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
-                         IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) 
+                         IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
                  ... | tri≈ ¬a b ¬c = b
                  ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
-                         IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) 
+                         IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
 
-                 union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b 
+                 union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b
                  union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
                       z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w
-                      z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+                      z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
                       z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
-                          u<b : u o< b  
+                          u<b : u o< b
                           u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb )
                       z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w
-                      z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+                      z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
                       z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
-                          u<a : u o< a 
+                          u<a : u o< a
                           u<a = supf-inject0 supf1-mono ( osucprev (begin
                              osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
                              osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
@@ -1153,18 +1153,18 @@
                  zo≤sz {z} z≤x with osuc-≡< z≤x
                  ... | case2 z<x = subst (λ k → z o≤ k) (sym (sf1=sf0 (zc-b<x _ z<x ))) (ZChain.zo≤sz zc (zc-b<x _ z<x ))
                  ... | case1 refl with osuc-≡< (supf1-mono (o<→≤ (px<x))) --   px o≤ supf1 px o≤ supf1 x ≡ sp1 → x o≤ sp1
-                 ... | case2 lt = begin 
-                     x ≡⟨ sym (Oprev.oprev=x op) ⟩ 
-                     osuc px ≤⟨ osucc (ZChain.zo≤sz zc o≤-refl)  ⟩ 
-                     osuc (supf0 px) ≡⟨ sym (cong osuc (sf1=sf0 o≤-refl )) ⟩ 
-                     osuc (supf1 px) ≤⟨ osucc lt ⟩ 
+                 ... | case2 lt = begin
+                     x ≡⟨ sym (Oprev.oprev=x op) ⟩
+                     osuc px ≤⟨ osucc (ZChain.zo≤sz zc o≤-refl)  ⟩
+                     osuc (supf0 px) ≡⟨ sym (cong osuc (sf1=sf0 o≤-refl )) ⟩
+                     osuc (supf1 px) ≤⟨ osucc lt ⟩
                      supf1 x ∎ where open o≤-Reasoning O
                  ... | case1 spx=sx with osuc-≡< ( ZChain.zo≤sz zc o≤-refl )
                  ... | case2 lt = begin
-                     x ≡⟨ sym (Oprev.oprev=x op) ⟩  
-                     osuc px ≤⟨ osucc lt ⟩ 
-                     supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩ 
-                     supf1 px ≤⟨ supf1-mono (o<→≤ px<x)  ⟩ 
+                     x ≡⟨ sym (Oprev.oprev=x op) ⟩
+                     osuc px ≤⟨ osucc lt ⟩
+                     supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
+                     supf1 px ≤⟨ supf1-mono (o<→≤ px<x)  ⟩
                      supf1 x ∎ where open o≤-Reasoning O
                  ... | case1 px=spx =  ⊥-elim ( <<-irr zc40 (proj1 ( mf< (supf0 px) (ZChain.asupf zc))) ) where
                      zc37 : supf0 px ≡ px
@@ -1175,8 +1175,8 @@
                        supf1 px ≡⟨ spx=sx ⟩
                        supf1 x ≡⟨ sf1=sp1 px<x ⟩
                        sp1 ∎ where open ≡-Reasoning
-                     zc40 :  f (supf0 px) ≤ supf0 px                        
-                     zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) 
+                     zc40 :  f (supf0 px) ≤ supf0 px
+                     zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39)
                            ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
 
                  order : {a b : Ordinal} {w : Ordinal} →
@@ -1188,22 +1188,22 @@
                      a≤px with trio< a px
                      ... | tri< a ¬b ¬c = o<→≤ a
                      ... | tri≈ ¬a b ¬c = o≤-refl0 b
-                     ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op)) 
+                     ... | 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
                      z20 : w ≤ supf1 b
                      z20 with trio< b px
-                     ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) 
-                          (fcup fc (o<→≤ (ordtrans a<b b<px))) 
-                     ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where 
+                     ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb)
+                          (fcup fc (o<→≤ (ordtrans a<b b<px)))
+                     ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where
                           a≤x : a o≤ x
                           a≤x = o<→≤ (ordtrans ( subst (λ k → a o< k ) b=px a<b ) px<x )
-                          z26 : odef ( UnionCF A f ay supf0 b ) w 
+                          z26 : odef ( UnionCF A f ay supf0 b ) w
                           z26 with x<y∨y≤x (supf1 a) b
                           ... | case2 b≤sa = z27 where
                               z27 : odef (UnionCF A f ay supf0 b) w
                               z27 with osuc-≡< b≤sa
-                              ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x 
-                                    ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px)))  sa<sb) )) 
+                              ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x
+                                    ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px)))  sa<sb) ))
                                        (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where
                                   x≤sa : x o≤ supf1 a
                                   x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa )
@@ -1215,13 +1215,13 @@
                                     supf0 (supf0 a) ≡⟨ cong supf0 (sym (sf1=sf0 a≤px )) ⟩
                                     supf0 (supf1 a) ≡⟨ cong supf0 (sym b=sa) ⟩
                                     supf0 b ∎ where open ≡-Reasoning
-                          ... | case1 sa<b with cfcs a<b b≤x sa<b fc  
-                          ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
+                          ... | case1 sa<b with cfcs a<b b≤x sa<b fc
+                          ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫
                           ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px)) su=u) (fcup fc u≤px)  ⟫ where
-                              u≤px : u o≤ px 
+                              u≤px : u o≤ px
                               u≤px = o<→≤ ( subst (λ k → u o< k ) b=px u<x )
                      ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b
-                     ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) 
+                     ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc)))
                      ... | case2 b≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
                           b=x : b ≡ x
                           b=x with trio< b x
@@ -1231,14 +1231,14 @@
                           a≤x : a o≤ x
                           a≤x = o<→≤ ( subst (λ k → a o< k ) b=x a<b )
                           sf1b=sp1 : supf1 b ≡ sp1
-                          sf1b=sp1  = sf1=sp1 (subst (λ k → px o< k) (trans (Oprev.oprev=x op) (sym b=x))  <-osuc) 
+                          sf1b=sp1  = sf1=sp1 (subst (λ k → px o< k) (trans (Oprev.oprev=x op) (sym b=x))  <-osuc)
                           z27 : supf1 a ≡ sp1
-                          z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa)  
+                          z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa)
                               b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1)  sa<sb )  ) ) sf1b=sp1
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-     ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? 
+     ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ?
               ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
               ; zo≤sz = ? ; is-minsup = ? ; cfcs = ?    } where
               mf : ≤-monotonic-f A f
@@ -1262,7 +1262,7 @@
           supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
 
           pchainU : HOD
-          pchainU = UnionIC A f ay supfz 
+          pchainU = UnionIC A f ay supfz
 
           zeq : {xa xb z : Ordinal }
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
@@ -1279,7 +1279,7 @@
 
           pic<x : {z : Ordinal } → (ic : IChain ay supfz z ) → osuc (IChain-i ic) o< x
           pic<x {z} (ic-init fc) = ob<x lim 0<x   -- 0<x ∧ lim x → osuc o∅ o< x
-          pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x 
+          pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x
 
           pchainU⊆chain : {z : Ordinal } → (pz : odef pchainU z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
           pchainU⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
@@ -1289,33 +1289,33 @@
                uz03 : ZChain.supf (pzc (ob<x lim ia<x)) ia o≤ ia
                uz03 = sa<x
 
-          chain⊆pchainU : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainU w 
+          chain⊆pchainU : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainU w
           chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
-          chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ 
+          chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫
              = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ  k → FClosure A f k w ) su=su fc) ⟫ where
                  u<x : u o< x
                  u<x = ordtrans u<oz oz<x
                  su=su : ZChain.supf (pzc oz<x) u ≡ supfz u<x
                  su=su = sym ( zeq _ _  (osucc u<oz) (o<→≤ <-osuc) )
                  su≡u :  supfz u<x ≡ u
-                 su≡u = begin 
+                 su≡u = begin
                     ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩
                     ZChain.supf (pzc oz<x) u  ≡⟨ su=u ⟩
-                    u ∎ where open ≡-Reasoning 
+                    u ∎ where open ≡-Reasoning
 
-          chain⊆pchainU1 : {z w : Ordinal } → (z<x : z o< x) → odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim z<x))) z) w → odef pchainU w 
+          chain⊆pchainU1 : {z w : Ordinal } → (z<x : z o< x) → odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim z<x))) z) w → odef pchainU w
           chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
-          chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ 
+          chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫
              = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ  k → FClosure A f k w ) su=su fc) ⟫ where
                  u<x : u o< x
                  u<x = ordtrans u<oz z<x
                  su=su : ZChain.supf (pzc (ob<x lim z<x)) u ≡ supfz u<x
                  su=su = sym ( zeq _ _  (o<→≤ (osucc u<oz)) (o<→≤ <-osuc) )
                  su≡u :  supfz u<x ≡ u
-                 su≡u = begin 
+                 su≡u = begin
                     ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩
                     ZChain.supf (pzc (ob<x lim z<x)) u  ≡⟨ su=u ⟩
-                    u ∎ where open ≡-Reasoning 
+                    u ∎ where open ≡-Reasoning
 
           ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b }
             → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib)
@@ -1324,29 +1324,29 @@
                  uz11 : IChain-i ia o< IChain-i ib
                  uz11 with trio< (IChain-i ia ) (IChain-i ib)
                  ... | tri< a ¬b ¬c = a
-                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (trans (zeq _ _ (o≤-refl0 (cong osuc b)) (o<→≤ <-osuc) ) 
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (trans (zeq _ _ (o≤-refl0 (cong osuc b)) (o<→≤ <-osuc) )
                      ( cong (ZChain.supf (pzc (pic<x ib))) b )) sa<sb )
                  ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin
-                     ZChain.supf (pzc (pic<x ib)) (IChain-i ib)  ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc)  ⟩ 
-                     ZChain.supf (pzc (pic<x ia)) (IChain-i ib)  ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ 
+                     ZChain.supf (pzc (pic<x ib)) (IChain-i ib)  ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc)  ⟩
+                     ZChain.supf (pzc (pic<x ia)) (IChain-i ib)  ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩
                      ZChain.supf (pzc (pic<x ia)) (IChain-i ia)  ∎ ) sa<sb ) where open o≤-Reasoning O
 
           IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b )
               → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a
           IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫
           IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where
-               ic02 : o∅ o< supfz i<x 
-               ic02 = ZChain.0<supfz (pzc  (ob<x lim i<x)) 
+               ic02 : o∅ o< supfz i<x
+               ic02 = ZChain.0<supfz (pzc  (ob<x lim i<x))
                ic01 : o∅ o< i
                ic01 = ordtrans<-≤ ic02 sa<x
-          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib 
+          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib
               = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x)
                   (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc )
 
           ptotalU : IsTotalOrderSet pchainU
           ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
-          ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib) 
-          ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib) 
+          ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib)
+          ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib)
           ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
 
           usup : MinSUP A pchainU
@@ -1400,7 +1400,7 @@
           supf1 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z   -- each sup o< x
           ... | tri≈ ¬a b ¬c = spu                                 -- sup of all sup o< x
-          ... | tri> ¬a ¬b c = sps                                 -- sup of spu which o< x 
+          ... | tri> ¬a ¬b c = sps                                 -- sup of spu which o< x
                                                 --  if x o< spu, spu is not included in UnionCF x
           -- the chain
 
@@ -1417,9 +1417,9 @@
 
           sf1=spu : {z : Ordinal } → x ≡ z → supf1 z ≡ spu
           sf1=spu {z} eq with trio< z x
-          ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym eq)) 
+          ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym eq))
           ... | tri≈ ¬a b ¬c = refl
-          ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym eq)) 
+          ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym eq))
 
           sf1=sps : {z : Ordinal } → (a : x o< z ) → supf1 z ≡ sps
           sf1=sps {z} x<z with trio< z x
@@ -1444,7 +1444,7 @@
 
           asupf : {z : Ordinal } → odef A (supf1 z)
           asupf {z} with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.asupf (pzc  (ob<x lim a)) 
+          ... | tri< a ¬b ¬c = ZChain.asupf (pzc  (ob<x lim a))
           ... | tri≈ ¬a b ¬c = MinSUP.as usup
           ... | tri> ¬a ¬b c = MinSUP.as ssup
 
@@ -1457,18 +1457,18 @@
                   supf1 z ≡⟨ sf1=sf (ordtrans≤-< z≤y y<x)  ⟩
                   ZChain.supf (pzc  (ob<x lim (ordtrans≤-< z≤y y<x))) z ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc)  ⟩
                   ZChain.supf (pzc  (ob<x lim y<x)) z ≤⟨ ZChain.supf-mono (pzc  (ob<x lim y<x)) z≤y  ⟩
-                  ZChain.supf (pzc  (ob<x lim y<x)) y ∎ 
+                  ZChain.supf (pzc  (ob<x lim y<x)) y ∎
           ... | tri≈ ¬a b ¬c = zc01 where  -- supf1 z o≤ spu
                open o≤-Reasoning O
                zc01 : supf1 z o≤ spu
                zc01 with osuc-≡< (subst (λ k → z o≤ k) b z≤y)
                ... | case1 z=x = o≤-refl0 (sf1=spu (sym z=x))
-               ... | case2 z<x = subst (λ k → k o≤ spu ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) 
+               ... | case2 z<x = subst (λ k → k o≤ spu ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) )
                  (MinSUP.as usup) (λ uw → MinSUP.x≤sup usup (chain⊆pchainU1 z<x uw)) )
           ... | tri> ¬a ¬b c = zc01 where  -- supf1 z o≤ sps
                zc01 : supf1 z o≤ sps
                zc01 with trio< z x
-               ... | tri< z<x ¬b ¬c = IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) 
+               ... | tri< z<x ¬b ¬c = IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) )
                  (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 (chain⊆pchainU1 z<x uw)) )
                ... | tri≈ ¬a z=x ¬c = MinSUP.minsup usup (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 uw) )
                ... | tri> ¬a ¬b c = o≤-refl -- (sf1=sps c)
@@ -1479,23 +1479,23 @@
           is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
           is-minsup {z} z≤x with osuc-≡< z≤x
           ... | case1 z=x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
-               zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z 
-               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ ) 
-               zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x)))  
+               zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z
+               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ )
+               zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x)))
                    ( MinSUP.x≤sup usup  ⟪ az , ic-isup u u<x (o≤-refl0 zm05) (subst (λ k → FClosure A f k w) (sym zm06) fc)  ⟫  ) where
                        u<x : u o< x
                        u<x = subst (λ k → u o< k) z=x u<b
                        zm06 : supfz (subst (λ k → u o< k) z=x u<b) ≡ supf1 u
                        zm06 = trans (zeq _ _  o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<x ))
-                       zm05 : supfz (subst (λ k → u o< k) z=x u<b) ≡ u 
+                       zm05 : supfz (subst (λ k → u o< k) z=x u<b) ≡ u
                        zm05 = trans zm06 su=u
                zm01 : { s : Ordinal } → odef A s →  ( {x : Ordinal  } → odef (UnionCF A f ay supf1 z) x → x ≤ s )  → supf1 z o≤ s
-               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where 
+               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where
                    zm02 : {w : Ordinal } →  odef pchainU w → w ≤ s
                    zm02 {w} uw with pchainU⊆chain uw
-                   ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ 
+                   ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫
                    ... | ⟪ az , ch-is-sup u1 u<b su=u fc ⟫ = sup  ⟪ az , ch-is-sup u1 (ordtrans u<b zm05) (trans zm03 su=u) zm04 ⟫  where
-                       zm05 : osuc (IChain-i (proj2 uw)) o< z 
+                       zm05 : osuc (IChain-i (proj2 uw)) o< z
                        zm05 = subst (λ k → osuc  (IChain-i (proj2 uw)) o< k) (sym z=x) ( pic<x (proj2 uw) )
                        u<x : u1 o< x
                        u<x = subst (λ k → u1 o< k) z=x ( ordtrans u<b zm05 )
@@ -1504,21 +1504,21 @@
                        zm04 : FClosure A f (supf1 u1) w
                        zm04 = subst (λ k → FClosure A f k w) (sym zm03) fc
           ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
-               supf0 = ZChain.supf (pzc (ob<x lim z<x)) 
+               supf0 = ZChain.supf (pzc (ob<x lim z<x))
                msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
                msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc)
                s1=0 : {u : Ordinal } → u o< z → supf1 u ≡ supf0 u
-               s1=0 {u} u<z = trans (sf1=sf (ordtrans u<z z<x)) (zeq _ _ (o<→≤ (osucc u<z))  (o<→≤ <-osuc) ) 
-               zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z 
-               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup  ⟪ az , ch-init fc ⟫ ) 
-               zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) 
+               s1=0 {u} u<z = trans (sf1=sf (ordtrans u<z z<x)) (zeq _ _ (o<→≤ (osucc u<z))  (o<→≤ <-osuc) )
+               zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z
+               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup  ⟪ az , ch-init fc ⟫ )
+               zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x))
                   ( IsMinSUP.x≤sup msup  ⟪ az , ch-is-sup u u<b (trans (sym (s1=0 u<b)) su=u)  (subst (λ k → FClosure A f k w) (s1=0 u<b) fc)  ⟫  )
                zm01 : { s : Ordinal } → odef A s →  ( {x : Ordinal  } → odef (UnionCF A f ay supf1 z) x → x ≤ s )  → supf1 z o≤ s
-               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where 
+               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where
                    zm02 : {w : Ordinal } →  odef (UnionCF A f ay supf0 z) w → w ≤ s
                    zm02 {w} ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫
-                   zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup  
-                       ⟪ az , ch-is-sup u u<b (trans (s1=0 u<b) su=u) (subst (λ k → FClosure A f k w) (sym (s1=0 u<b)) fc) ⟫  
+                   zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup
+                       ⟪ az , ch-is-sup u u<b (trans (s1=0 u<b) su=u) (subst (λ k → FClosure A f k w) (sym (s1=0 u<b)) fc) ⟫
 
 
 
@@ -1558,11 +1558,11 @@
                        osuc m ≤⟨ osucc m<x ⟩
                        x ≡⟨ sym b=x ⟩
                        b ∎ ) where open o≤-Reasoning O
-                   zc45 : supf1 u ≡  ZChain.supf (pzc  (ob<x lim m<x)) u 
+                   zc45 : supf1 u ≡  ZChain.supf (pzc  (ob<x lim m<x)) u
                    zc45 = begin
                        supf1 u ≡⟨ sf1=sf (subst (λ k → u o< k) b=x u<b )  ⟩
                        ZChain.supf (pzc  (ob<x lim (subst (λ k → u o< k) b=x u<b ))) u  ≡⟨ zeq _ _ (osucc u<x) (o<→≤ <-osuc)  ⟩
-                       ZChain.supf (pzc  (ob<x lim m<x)) u ∎  where open ≡-Reasoning 
+                       ZChain.supf (pzc  (ob<x lim m<x)) u ∎  where open ≡-Reasoning
                    zc44 : FClosure A f (supf1 u) w
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
@@ -1580,17 +1580,33 @@
                zc40 with zcb
                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
                ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u u<x (trans zc45 su=u) zc44  ⟫ where
-                   zc45 : supf1 u ≡  ZChain.supf (pzc  (ob<x lim b<x)) u 
+                   zc45 : supf1 u ≡  ZChain.supf (pzc  (ob<x lim b<x)) u
                    zc45 = begin
                        supf1 u ≡⟨ sf1=sf (ordtrans u<x b<x)  ⟩
                        ZChain.supf (pzc  (ob<x lim (ordtrans u<x b<x) )) u  ≡⟨ zeq _ _ (o<→≤ (osucc u<x)) (o<→≤ <-osuc)  ⟩
-                       ZChain.supf (pzc  (ob<x lim b<x )) u ∎  where open ≡-Reasoning 
+                       ZChain.supf (pzc  (ob<x lim b<x )) u ∎  where open ≡-Reasoning
                    zc44 : FClosure A f (supf1 u) w
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
           order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
-          order = ?
-
+          order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x
+          ... | case2 b<x = subst (λ k → w ≤ k ) (sym (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl ))))  (
+             ZChain.order (pzc b<x) o≤-refl
+                  (subst₂ (λ j k → j o< k ) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc)))
+                      (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl)))  sa<sb)
+                  (subst  (λ k → FClosure A f k w) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc)) )  fc ) ) where
+               a<b : a o< b
+               a<b = supf-inject0 supf-mono sa<sb
+               a<x : a o< x
+               a<x = ordtrans<-≤ a<b b≤x
+          ... | case1 refl = zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb)
+                   (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc ) where
+               a<x : a o< x
+               a<x = supf-inject0 supf-mono sa<sb
+               zc40 : ZChain.supf (pzc  (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc  (ob<x lim a<x )) a) w → w ≤ spu
+               zc40 sa<sp fc = MinSUP.x≤sup usup ⟪ A∋fc _ f mf fc , ic-isup a a<x zc44 fc ⟫ where
+                     zc44 : supfz a<x o≤ a
+                     zc44 = ?
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function