--- a/src/zorn.agda	Wed Nov 02 03:42:53 2022 +0900
+++ b/src/zorn.agda	Wed Nov 02 13:53:10 2022 +0900
@@ -243,6 +243,8 @@
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
    field
       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+      minsup : { sup1 : Ordinal } → odef A sup1 
+         →  ( {z : Ordinal  } → odef B z → (z ≡ sup1 ) ∨ (z << sup1 ))  → x o≤ sup1
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -659,7 +661,15 @@
                     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) (chain-mono1 (o<→≤ b<x) uz) }  , m04 ⟫
+                      ⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz)
+                          ; minsup = m07 }  , m04 ⟫ where
+                             m10 : {s : Ordinal }  →  (odef A s ) 
+                                →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 
+                                →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
+                             m10 = ?
+                             m07 :  {sup1 : Ordinal} → odef A sup1 → ({z : Ordinal} →
+                                 odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ sup1) ∨ (z << sup1)) → b o≤ sup1
+                             m07 {s} as min = IsSup.minsup (proj2 is-sup) as (m10 as min)
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -692,7 +702,8 @@
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫    -- ZChain on x
+                      ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )
+                         ; minsup = ? } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -725,7 +736,7 @@
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
      ind f mf {y} ay x prev with Oprev-p x
-     ... | yes op = zc4 where
+     ... | yes op = zc41 where
           --
           -- we have previous ordinal to use induction
           --
@@ -755,63 +766,69 @@
           ... | 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  ⟫ ) 
 
-          zc41 : supf0 px o< x →  ZChain A f mf ay x 
-          zc41 sfpx<x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
+          --
+          -- find the next value of supf
+          --
+
+          pchainpx : HOD
+          pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) 
+                ∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
+               zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 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 ∧ UChain A f mf ay supf0 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 (cong (&) 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 ∧ UChain A f mf ay supf0 px 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 ) 
+ 
+          ptotal : IsTotalOrderSet pchainpx
+          ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso 
+                   (chain-total A f mf ay supf0 (proj2 a) (proj2 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
+               eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+          ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
+               lt1 : a0 < b0
+               lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+          ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
+          ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
+               eq1 : a0 ≡ b0
+               eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+          ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
+               lt1 : a0 < b0
+               lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+          ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b)
+ 
+          pcha : pchainpx ⊆' A
+          pcha (case1 lt) = proj1 lt
+          pcha (case2 fc) = A∋fc _ f mf fc
+ 
+          sup1 : MinSUP A pchainpx 
+          sup1 = minsupP pchainpx pcha ptotal
+          sp1 = MinSUP.sup sup1
+
+          --
+          --     supf0 px o≤ sp1
+          --  
+ 
+          zc41 : ZChain A f mf ay x 
+          zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
+          zc41 | (case2 sfpx<sp1) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
-                 --  supf0 px is included by the chain
+                 --  supf0 px is included by the chain of sp1
                  --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 
                  --  supf1 x ≡ sp1, which is not included now
 
-                 pchainpx : HOD
-                 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) 
-                       ∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
-                      zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 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 )
-                 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → odef A z
-                 zc01 {z} (case1 lt) = proj1 lt 
-                 zc01 {z} (case2 fc) = ( A∋fc (supf0 px) f mf fc )
-
-                 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 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 (cong (&) 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 ∧ UChain A f mf ay supf0 px 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 ) 
-
-                 ptotal : IsTotalOrderSet pchainpx
-                 ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso 
-                          (chain-total A f mf ay supf0 (proj2 a) (proj2 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
-                      eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
-                 ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
-                      lt1 : a0 < b0
-                      lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-                 ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
-                 ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
-                      eq1 : a0 ≡ b0
-                      eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
-                 ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
-                      lt1 : a0 < b0
-                      lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-                 ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b)
-
-                 pcha : pchainpx ⊆' A
-                 pcha (case1 lt) = proj1 lt
-                 pcha (case2 fc) = A∋fc _ f mf fc
-
-                 sup1 : MinSUP A pchainpx 
-                 sup1 = minsupP pchainpx pcha ptotal
-                 sp1 = MinSUP.sup sup1
-
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
@@ -943,11 +960,13 @@
                                 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
                         ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px  ⟫ )
                  zc12 {z} (case2 fc) = zc21 fc where
+                        zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px )
+                        zc20 = ?
                         zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 
-                        zc21 (init asp refl ) with  osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
+                        zc21 (init asp refl ) with  zc20
                         ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px zc18 
                                      record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
                               zc15 : supf1 px ≡ px
@@ -976,7 +995,7 @@
 
                         ... | case2 sfp<px  with ZChain.csupf zc sfp<px --  odef (UnionCF A f mf ay supf0 px) (supf0 px)
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ 
-                        ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ?  
+                        ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18  
                               record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫  where
                                  z10 :  {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) 
                                  z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc)
@@ -992,6 +1011,8 @@
                                        lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt
                                  z12 : supf1 u ≡ u
                                  z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup)
+                                 zc18 : supf1 u o< supf1 x
+                                 zc18 = ?
 
 
 
@@ -1055,17 +1076,13 @@
                            cs05 : px o< supf0 px
                            cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
                            cs06 : supf0 px o< osuc px
-                           cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x 
+                           cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ?
                      csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
                      csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? 
                      -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
 
 
-          zc4 : ZChain A f mf ay x     --- x o≤ supf px 
-          zc4 with trio< x (supf0 px)
-          ... | tri> ¬a ¬b c = zc41 c
-          ... | tri≈ ¬a b ¬c = ?
-          ... | tri< a ¬b ¬c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
+          zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
 
                  --  supf0 px not is included by the chain
@@ -1145,7 +1162,7 @@
                         zc12 = subst  (λ k → supf0 k ≡ u1) eq ?
                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                         zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
-                                 ; is-sup = record { x≤sup = x≤sup } }
+                                 ; is-sup = record { x≤sup = x≤sup ; minsup = ? } }
                  zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
@@ -1197,8 +1214,8 @@
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
                  ... | tri> ¬a ¬b px<b = zc31 ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -1207,7 +1224,7 @@
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt → 
-                        IsSup.x≤sup (proj1 is-sup) ?} } 
+                        IsSup.x≤sup (proj1 is-sup) ? ; minsup = ? } } 
                      zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
                      zc31 (case1 ¬sp=x) with zc30
                      ... | refl = ⊥-elim (¬sp=x zcsup )
@@ -1366,7 +1383,7 @@
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
                z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
-               z19 = record {   x≤sup = z20 }  where
+               z19 = record {   x≤sup = z20 ; minsup = ? }  where
                    z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
                    z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy)
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
@@ -1496,7 +1513,8 @@
           sc=c : supf mc ≡ mc
           sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
               is-sup :  IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
-              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )} 
+              is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )
+                          ; minsup = ? } 
               not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx)
               not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where 
                    z30 : * mc < * (cf nmx mc)
@@ -1515,7 +1533,7 @@
                    z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
 
           is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
-          is-sup = record { x≤sup = z22 } where
+          is-sup = record { x≤sup = z22 ; minsup = ? } where
                 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
                 z23 lt = MinSUP.x≤sup spd lt
                 z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →