# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670112912 -32400
# Node ID 912ca4abe8067375f75d01def946915829643a52
# Parent  f12a9b4066a0f2668ac973f565f648d75fb0c0ad
pxhainx conditon is requied?

diff -r f12a9b4066a0 -r 912ca4abe806 src/zorn.agda
--- a/src/zorn.agda	Sat Dec 03 16:57:15 2022 +0900
+++ b/src/zorn.agda	Sun Dec 04 09:15:12 2022 +0900
@@ -23,7 +23,7 @@
 import BAlgbra
 
 open import Data.Nat hiding ( _<_ ; _≤_ )
-open import Data.Nat.Properties 
+open import Data.Nat.Properties
 open import nat
 
 
@@ -76,7 +76,7 @@
 
 ftrans<-≤ : {x y z : Ordinal } →  x <<  y →  y ≤ z →  x <<  z
 ftrans<-≤ {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y
-ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt 
+ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt
 
 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
@@ -168,7 +168,7 @@
           fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → * (f x)  ≡ * y1
           fc03 y1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x)
           fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) )
-          ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) (cong (*) eq) 
+          ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) (cong (*) eq)
           ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where
                fc05 : * x ≡ * y1
                fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
@@ -258,7 +258,7 @@
 --    this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal.
 --
 
-fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal } 
+fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal }
     → (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a
 fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl ))
 ... | case1 eq = trans eq (sym a=b)
@@ -269,16 +269,16 @@
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
--- Union of supf z and FClosure A f y 
+-- Union of supf z and FClosure A f y
 
-data UChain  { A : HOD } { f : Ordinal → Ordinal }  {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) 
+data UChain  { A : HOD } { f : Ordinal → Ordinal }  {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y )
        (x : Ordinal) : (z : Ordinal) → Set n where
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z
     ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z
 
 UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
 UnionCF A f ay supf x
-   = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;   
+   = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 
@@ -324,8 +324,8 @@
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
         → odef (UnionCF A f ay supf a) c → odef (UnionCF A f ay supf b) c
-chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
-chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ 
+chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫
+chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
@@ -340,7 +340,7 @@
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
-      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) 
+      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
            → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b
 
@@ -352,14 +352,14 @@
    chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y
    chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
 
-   mf : ≤-monotonic-f A f 
+   mf : ≤-monotonic-f A f
    mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
       mf00 : * x < * (f x)
       mf00 = proj1 ( mf< x ax )
 
    f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a)
-   f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫ 
-   f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-is-sup u su<x su=u (fsuc _ fc) ⟫ 
+   f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫
+   f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-is-sup u su<x su=u (fsuc _ fc) ⟫
 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
    supf-inject {x} {y} sx<sy with trio< x y
@@ -382,7 +382,7 @@
    supf-is-minsup _ = refl
 
    -- different from order because y o< supf
-   fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) 
+   fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u )
    fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
@@ -390,7 +390,7 @@
 
    initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x →  y ≤ x
    initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc
-   initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc)  
+   initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc)
 
    f-total : IsTotalOrderSet chain
    f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
@@ -400,35 +400,35 @@
          ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) a₁ fca ) (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)
-                  ct00 = cong (*) eq1  
-         ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  
-         fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb 
+                  ct00 = cong (*) eq1
+         ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
+         fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
          fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) c fcb ) (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)
-                  ct00 = cong (*) (sym eq1)  
+                  ct00 = cong (*) (sym eq1)
          ... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
    f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
       ft01 : (& a) ≤ (& b) → Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
-         a=b : a ≡ b 
+         a=b : a ≡ b
          a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq)
       ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  where
-         a<b : a < b 
+         a<b : a < b
          a<b = subst₂ (λ j k → j < k ) *iso *iso lt
       ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb))
    f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where
       ft01 : (& b) ≤ (& a) → Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
-         a=b : a ≡ b 
+         a=b : a ≡ b
          a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq))
       ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where
-         b<a : b < a 
+         b<a : b < a
          b<a = subst₂ (λ j k → j < k ) *iso *iso lt
       ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
-   f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =  
+   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 )
 
    IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
@@ -444,10 +444,10 @@
        fsp≤sp : f sp ≤  sp
        fsp≤sp = subst (λ k → f k ≤ sp ) (sym (HasPrev.x=fy hp)) im00
 
-   supf-¬hp : {x  : Ordinal } → x o≤ z 
+   supf-¬hp : {x  : Ordinal } → x o≤ z
        → ( {a : Ordinal } → odef A a → a << f a )
        → ¬ ( HasPrev A (UnionCF A f ay supf x) f (supf x) )
-   supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → 
+   supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw →
        (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
 
    supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
@@ -458,7 +458,7 @@
                su<b : u o< b
                su<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  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
+       z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf  ; x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
 
    -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
    --    the condition of cfcs is satisfied, this is obvious
@@ -479,27 +479,27 @@
 
 record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
   field
-     i : Ordinal  
+     i : Ordinal
      i<x : i o< x
-     fc : FClosure A f (supfz i<x) z 
+     fc : FClosure A f (supfz i<x) z
 
 --
 -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup
 --
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
-        {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb ) 
+        {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb )
       → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
 supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
        supfa = ZChain.supf za
        supfb = ZChain.supf zb
        ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
        ind x prev x≤xa = sxa=sxb where
-           ma = ZChain.minsup za x≤xa 
+           ma = ZChain.minsup za x≤xa
            mb = ZChain.minsup zb (OrdTrans x≤xa xa≤xb )
            spa = MinSUP.sup ma
            spb = MinSUP.sup mb
            sax=spa : supfa x ≡ spa
-           sax=spa = ZChain.supf-is-minsup za x≤xa 
+           sax=spa = ZChain.supf-is-minsup za x≤xa
            sbx=spb : supfb x ≡ spb
            sbx=spb = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb )
            sxa=sxb : supfa x ≡ supfb x
@@ -509,11 +509,11 @@
                begin
                  supfb x  ≡⟨ sbx=spb ⟩
                  spb  ≤⟨ MinSUP.minsup mb (MinSUP.as ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
-                 spa ≡⟨ sym sax=spa ⟩ 
-                 supfa x ∎ ) a ) where 
+                 spa ≡⟨ sym sax=spa ⟩
+                 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 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                    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 )
@@ -524,10 +524,10 @@
                  supfa x  ≡⟨ sax=spa ⟩
                  spa  ≤⟨ MinSUP.minsup ma (MinSUP.as mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
                  spb  ≡⟨ sym sbx=spb ⟩
-                 supfb x ∎ ) c ) where 
+                 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 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                    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 ))
@@ -606,9 +606,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 bw 
-             ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq)) 
-             ... | case2 lt = case2 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
 
@@ -659,7 +659,7 @@
         supf = ZChain.supf zc
 
         zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf< ay zc x
-        zc1 x x≤A with Oprev-p x  
+        zc1 x x≤A with Oprev-p x
         ... | yes op = record { is-max = is-max } where
                px = Oprev.oprev op
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a →
@@ -682,7 +682,7 @@
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
-                  m18 : supf x ≡ MinSUP.sup m17 
+                  m18 : supf x ≡ MinSUP.sup m17
                   m18 = ZChain.supf-is-minsup zc x≤A
                   m10 : f (supf b) ≡ supf b
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
@@ -722,7 +722,7 @@
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
-                  m18 : supf x ≡ MinSUP.sup m17 
+                  m18 : supf x ≡ MinSUP.sup m17
                   m18 = ZChain.supf-is-minsup zc x≤A
                   m10 : f (supf b) ≡ supf b
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
@@ -799,7 +799,7 @@
           ... | case1 eq = case2 eq
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
 
-          mf : ≤-monotonic-f A f 
+          mf : ≤-monotonic-f A f
           mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
              mf00 : * x < * (f x)
              mf00 = proj1 ( mf< x ax )
@@ -920,7 +920,7 @@
                  sf≤ {z} x≤z with trio< z px
                  ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
                  ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
-                 ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c) 
+                 ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c)
                      (supf1-mono (o<→≤ c ))
                       --  px o<z → supf x ≡ supf0 px ≡ supf1 px o≤ supf1 z
 
@@ -931,22 +931,22 @@
 
                  sfpx<x : sp1 o≤ x → supf0 px o< x
                  sfpx<x sp1≤x with trio< (supf0 px) x
-                 ... | tri< a ¬b ¬c = a 
-                 ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
+                 ... | tri< a ¬b ¬c = a
+                 ... | 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-≡< m13
                       ... | case1 eq = eq
-                      ... | case2 lt = ⊥-elim ( o≤> sp1≤x (subst (λ k → k o< sp1) spx=x lt )) 
+                      ... | case2 lt = ⊥-elim ( o≤> sp1≤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)  
+                          m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc)
                  ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp1≤x )))   -- x o< supf0 px o≤ sp1 ≤ x
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 cfcs : {a b w : Ordinal } 
+                 cfcs : {a b w : Ordinal }
                      → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
                  cfcs {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
                  ... | case2 px≤sa = z50 where
@@ -963,27 +963,27 @@
                           sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
                           spx=sa : supf0 px ≡ supf0 a
                           spx=sa = begin
-                                supf0 px ≡⟨ cong supf0 px=sa  ⟩ 
+                                supf0 px ≡⟨ cong supf0 px=sa  ⟩
                                 supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc a≤px sa≤px  ⟩
                                 supf0 a ∎  where open ≡-Reasoning
                           z51 : supf0 px o< b
-                          z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩ 
-                                supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 
+                          z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩
+                                supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩
                                 supf1 a ∎ )) sa<b where open ≡-Reasoning
                           z52 : supf1 a ≡ supf1 (supf0 px)
-                          z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 
-                                supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px sa≤px ) ⟩ 
-                                supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
-                                supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ 
+                          z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩
+                                supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px sa≤px ) ⟩
+                                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 
+                                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 : UChain ay b w
-                          cp = ch-is-sup (supf0 px) z51 z53 (subst (λ k → FClosure A f k w) z52 fc) 
+                          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
@@ -991,22 +991,22 @@
                  ... | tri< a<px ¬b ¬c = z50 where
                       z50 : odef (UnionCF A f ay supf1 b) w
                       z50 with osuc-≡< b≤x
-                      ... | case2 lt with ZChain.cfcs zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc  
-                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                      ... | case2 lt with ZChain.cfcs zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc
+                      ... | ⟪ 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 a<px o≤-refl sa<px fc  
-                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                           u<x = ordtrans<-≤ u<b b≤x
+                      z50 | case1 eq with ZChain.cfcs zc a<px o≤-refl sa<px fc
+                      ... | ⟪ 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 
+                      -- a ≡ px , b ≡ x, sp o≤ x
                       px<b : px o< b
                       px<b = subst₂ (λ j k → j o< k) a=px refl a<b
                       b=x : b ≡ x
@@ -1019,14 +1019,18 @@
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
                       csupf1 : odef (UnionCF A f ay supf1 b) w
-                      csupf1 = ⟪ 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 ?)
+                      csupf1 with zc43 px (supf0 px)
+                      ... | case2 spx≤px = ⟪ z53 , ch-is-sup (supf0 px) z54 z52 fc1 ⟫  where
+                          z54 : supf0 px o< b
+                          z54 = subst (λ k → supf0 px o< k ) (trans (Oprev.oprev=x op) (sym b=x) ) spx≤px
                           z52 : supf1 (supf0 px) ≡ supf0 px
-                          z52 = trans (sf1=sf0 (zc-b<x _ (sfpx<x ?))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (sfpx<x ?) ) )
-                          fc1 : FClosure A f (supf1 spx) w
+                          z52 = trans (sf1=sf0 spx≤px ) ( ZChain.supf-idem zc o≤-refl spx≤px  )
+                          fc1 : FClosure A f (supf1 (supf0 px)) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
+                      ... | case1 px<spx = ⊥-elim (¬p<x<op ⟪ px<spx , z54  ⟫ ) where  -- supf1 px o≤ spuf1 x → supf1 px ≡ x o< x
+                          z54 : supf0 px o≤ px
+                          z54 = subst₂ (λ j k → supf0 j o< k ) a=px (trans b=x (sym (Oprev.oprev=x op))) sa<b
+
                  ... | 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
@@ -1037,13 +1041,13 @@
                     ... | 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 ) with trio< (supf0 u) (supf0 px) 
+                    zc21 (init asp refl ) with trio< (supf0 u) (supf0 px)
                     ... | tri< a ¬b ¬c = case1 ⟪ asp , ch-is-sup u u<px (trans (sym (sf1=sf0 (o<→≤ u<px))) su=u )(init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
                         u<px :  u o< px
                         u<px =  ZChain.supf-inject zc a
                         asp0 : odef A (supf0 u)
                         asp0 = ZChain.asupf zc
-                    ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) 
+                    ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) )
                         (sym (trans (sf1=sf0 (zc-b<x _ u<x))  b )))
                     ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
 
@@ -1051,7 +1055,7 @@
                  is-minsup {z} z≤x with osuc-≡< z≤x
                  ... | case1 z=x = record { as = zc22 ; x≤sup = z23 ; minsup = z24  }  where
                     px<z : px o< z
-                    px<z = subst (λ k → px o< k) (sym z=x) px<x 
+                    px<z = subst (λ k → px o< k) (sym z=x) px<x
                     zc22 : odef A (supf1 z)
                     zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z ))  ( MinSUP.as sup1 )
                     z26 : supf1 px ≤ supf1 x
@@ -1059,29 +1063,33 @@
                     z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
                     z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz )
                     ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j  ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where
-                        z25 : w ≤ supf0 px 
-                        z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz 
+                        z25 : w ≤ supf0 px
+                        z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz
                     ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) )
-                    z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )                 
+                    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
-                        z25 : {w : Ordinal } → odef pchainpx w → w ≤ s 
+                        z25 : {w : Ordinal } → odef pchainpx w → w ≤ s
                         z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where
-                            z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x o≤ 
+                            -- z=x , supf0 px o< x
+                            z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x ≡ sp1 o≤ x ≡ z
                             z28 = subst (λ k → supf0 px o< k) (sym z=x) (sfpx<x ?)
-                            z29 : supf0 px o≤ px 
+                            z29 : supf0 px o≤ px
                             z29 = zc-b<x _ (sfpx<x ?)
                             z27 : supf1 (supf0 px) ≡ supf0 px
                             z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 )
                             fc1 : FClosure A f (supf1 (supf0 px)) w
                             fc1 = subst (λ k → FClosure A f k w) (sym z27) fc
+                            -- x o≤ supf0 px o≤ supf0 z ≡ supf0 x ≡ sp1
+                            --   x o≤ supf0 px o≤ supf0 x ≡ sp1
+                            --       fc : FClosure A f (supf0 px) w  --   ¬ ( supf0 px o< x ) → ¬ odef ( UnionCF A f ay supf1 z ) w
                         z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
                         z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc  ⟫) = sup ⟪ ua , ch-is-sup u u<z
                              (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where
-                                u≤px : u o< osuc px
-                                u≤px = ordtrans u<x <-osuc
-                                u<z : u o< z                                                                                         
-                                u<z = ordtrans u<x (subst (λ k → px o< k ) (sym z=x) px<x )
+                            u≤px : u o< osuc px
+                            u≤px = ordtrans u<x <-osuc
+                            u<z : u o< z
+                            u<z = ordtrans u<x (subst (λ k → px o< k ) (sym z=x) px<x )
                  ... | case2 z<x = record { as = zc22 ; x≤sup = z23 ; minsup = z24  } where
                     z≤px = zc-b<x _ z<x
                     m =  ZChain.is-minsup zc z≤px
@@ -1089,16 +1097,16 @@
                     zc22 = subst (λ k → odef A k ) (sym (sf1=sf0 z≤px))  ( IsMinSUP.as m )
                     z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
                     z23 {w} ⟪ ua , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) ( ZChain.fcy<sup zc z≤px fc )
-                    z23 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) 
+                    z23 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px))
                        (IsMinSUP.x≤sup m ⟪ 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 = ordtrans u<x z≤px
                     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=sf0 z≤px)) ( IsMinSUP.minsup m as z25 ) where
-                        z25 : {w : Ordinal } → odef ( UnionCF A f ay supf0 z ) w → w ≤ s 
+                        z25 : {w : Ordinal } → odef ( UnionCF A f ay supf0 z ) w → w ≤ s
                         z25 {w} ⟪ ua , ch-init fc ⟫ = sup ⟪ ua , ch-init fc ⟫
-                        z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc  ⟫ = sup ⟪ ua , ch-is-sup u u<x 
+                        z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc  ⟫ = sup ⟪ ua , ch-is-sup u u<x
                              (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where
                                 u≤px : u o≤ px
                                 u≤px = ordtrans u<x z≤px
@@ -1106,11 +1114,11 @@
                  order : {a b : Ordinal} {w : Ordinal} →
                     b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b
                  order {a} {b} {w} b≤x a<b fc with trio< b px
-                 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) )) 
+                 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) ))
                  ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
                  ... | tri> ¬a ¬b px<b with trio< a px
                  ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) sfpx≤sp1  --   supf1 a ≡ supf0 a
-                 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc ))  
+                 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc ))
                  ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where  --   supf1 a ≡ sp1
                      zc22 : a o< osuc px
                      zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
@@ -1126,21 +1134,21 @@
                      ... | case1 eq = sym (eq)
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                      zc31 : sp1 o≤ b
-                     zc31 = MinSUP.minsup sup1 ab zc32 where 
-                         zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) 
+                     zc31 = MinSUP.minsup sup1 ab zc32 where
+                         zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
                          zc32 = ?
-                     
+
      ... | no lim with trio< x o∅
-     ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 
+     ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
      ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
-              ; supfmax = ? ; is-minsup = ? ; cfcs = ?    }  
+              ; supfmax = ? ; is-minsup = ? ; cfcs = ?    }
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
               ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
-          -- mf : ≤-monotonic-f A f 
+          -- mf : ≤-monotonic-f A f
           -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust
 
-          mf : ≤-monotonic-f A f 
+          mf : ≤-monotonic-f A f
           mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
              mf00 : * x < * (f x)
              mf00 = proj1 ( mf< x ax )
@@ -1161,14 +1169,14 @@
           aic : {z : Ordinal } → IChain A f supfz z → odef A z
           aic {z} ic =  A∋fc _ f mf (IChain.fc ic )
 
-          zeq : {xa xb z : Ordinal } 
-             → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 
-             → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z  
-          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf< ay xa≤xb  
+          zeq : {xa xb z : Ordinal }
+             → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
+             → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z
+          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf< ay xa≤xb
               (pzc xa<x)  (pzc xb<x)  z≤xa
 
-          iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y 
-          iceq refl = cong supfz  o<-irr 
+          iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y
+          iceq refl = cong supfz  o<-irr
 
           ifc≤ : {za zb : Ordinal } ( ia : IChain A f supfz za ) ( ib : IChain A f supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib )
               → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za
@@ -1178,13 +1186,13 @@
           ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 with trio< (IChain.i ia)  (IChain.i ib)
-               ... | tri< ia<ib ¬b ¬c with 
+               ... | tri< ia<ib ¬b ¬c with
                     ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = cong (*) eq1
-               ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)  
-               uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) 
+               ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
+               uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
                uz01 | tri> ¬a ¬b ib<ia  with
                     ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
@@ -1198,7 +1206,7 @@
 
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z  
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
@@ -1212,7 +1220,7 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = ? --  chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
 
-          sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z  
+          sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z
           sf1=sf {z} z<x with trio< z x
           ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
@@ -1244,7 +1252,7 @@
 
           cfcs :  {a b w : Ordinal } → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
           cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
-          ... | case1 b=x with trio< a x 
+          ... | case1 b=x with trio< a x
           ... | tri< a<x ¬b ¬c = zc40 where
                sa = ZChain.supf (pzc  (ob<x lim a<x)) a
                m =  omax a sa     -- x is limit ordinal, so we have sa o< m o< x
@@ -1259,7 +1267,7 @@
                        osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
                        x ∎ ) where open o≤-Reasoning O
                ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
-               sam = ZChain.supf (pzc (ob<x lim m<x)) a 
+               sam = ZChain.supf (pzc (ob<x lim m<x)) a
                zc42 : osuc a o≤ osuc m
                zc42 = osucc (o<→≤ ( omax-x _ _ ) )
                sam<m : sam o< m
@@ -1270,29 +1278,29 @@
                zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-               ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫  
+               ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
-               supfb =  ZChain.supf (pzc (ob<x lim b<x)) 
-               sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a 
+               supfb =  ZChain.supf (pzc (ob<x lim b<x))
+               sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a
                sb=sa {a} a<b = trans (sf1=sf (ordtrans<-≤ a<b b≤x)) (zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ <-osuc) )
                fcb : FClosure A f (supfb a) w
-               fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc 
+               fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc
                --  supfb a o< b assures it is in Union b
                zcb : odef (UnionCF A f ay supfb b) w
                zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with zcb
-               ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫ 
+               ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫
 
           sup=u : {b : Ordinal} (ab : odef A b) →
                 b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
           sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
           ... | case1 b=x = ? where
                  zc31 : spu o≤ b
-                 zc31 = MinSUP.minsup usup ab zc32 where 
-                     zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b) 
+                 zc31 = MinSUP.minsup usup ab zc32 where
+                     zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b)
                      zc32 = ?
           ... | case2 b<x = trans (sf1=sf ?) (ZChain.sup=u (pzc (ob<x lim b<x)) ab ? ? )
      ---