--- a/src/zorn.agda	Sat Nov 19 00:04:35 2022 +0900
+++ b/src/zorn.agda	Sun Nov 20 08:36:24 2022 +0900
@@ -525,6 +525,34 @@
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
+spuf-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 ) 
+      → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
+spuf-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 = ? where
+           sax=m : supfa x ≡ MinSUP.sup (ZChain.minsup za x≤xa )
+           sax=m = ZChain.supf-is-minsup za x≤xa 
+           sbx=m : supfb x ≡ MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))
+           sbx=m = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb )
+           sxa=sxb : supfa x ≡ supfb x
+           sxa=sxb with trio< (supfa x) (supfb x)
+           ... | tri≈ ¬a b ¬c = b
+           ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (
+               begin
+                 supfb x  ≡⟨ ? ⟩
+                 MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))  ≤⟨ MinSUP.minsup ? ? ? ⟩
+                 MinSUP.sup (ZChain.minsup za x≤xa ) ≡⟨ ? ⟩ 
+                 supfa x ∎ ) a ) where open o≤-Reasoning O
+           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
+               begin
+                 supfa x  ≡⟨ ? ⟩
+                 MinSUP.sup (ZChain.minsup za x≤xa )  ≤⟨ MinSUP.minsup ? ? ? ⟩
+                 MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))  ≡⟨ ? ⟩
+                 supfb x ∎ ) c ) where open o≤-Reasoning O
+
 UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
         → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
@@ -831,6 +859,12 @@
            ax : odef A x
            is-sup : IsMinSUP A B f ax
 
+     zc43 : (x sp1 : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
+     zc43 x sp1 with trio< x sp1
+     ... | tri< a ¬b ¬c = case1 a
+     ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
+     ... | tri> ¬a ¬b c = case2 (o<→≤ c)
+
      --
      -- create all ZChains under o< x
      --
@@ -931,14 +965,8 @@
           --     supf0 px o≤ sp1
           --
 
-          zc43 : (x : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
-          zc43 x with trio< x sp1
-          ... | tri< a ¬b ¬c = case1 a
-          ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
-          ... | tri> ¬a ¬b c = case2 (o<→≤ c)
-
           zc41 : ZChain A f mf ay x
-          zc41 with zc43 x
+          zc41 with zc43 x sp1
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?  }  where
 
@@ -1007,11 +1035,8 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 --  supf0 a ≡ px we cannot use previous cfcs
+                 --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
                  --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-                 --    supf0 a o< sp1 ≡ x
-                 --    sp1 ≡ px ≡ supf0 a o< x
-                 --    sp1 o< px ≡ supf0 a → ⊥
                  -- 
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                      → a o< b → b o≤ x → supf1 a o< x  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
@@ -1255,79 +1280,34 @@
 
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z  
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
           pchain1 : HOD
           pchain1 = UnionCF A f mf ay supf1 x
 
-          is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-                b o< x → (ab : odef A b) →
-                HasPrev A (UnionCF A f mf ay supf x) f b  →
-                * a < * b → odef (UnionCF A f mf ay supf x) b
-          is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
-          ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
-          ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab ,
-                     -- subst (λ k → UChain A f mf ay supf x k )
-                     --     (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
-
-          zc70 : HasPrev A pchain f x  → ¬ xSUP pchain f x
-          zc70 pr xsup = ?
+          sfpx<=spu : {z : Ordinal } → supf1 z <= spu
+          sfpx<=spu {z} = ? -- MinSUP.x≤sup usup (case2 (init (ZChain.asupf zc {px}) refl ))
 
-          no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) supf0 x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = ? where -- record { supf = supf1  ; sup=u = sup=u
-               -- ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
-                 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
-                 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
-                 pchain0=1 : pchain ≡ pchain1
-                 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
-                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
-                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                     zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where
-                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
-                          zc12 (fsuc x fc) with zc12 fc
-                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-                          ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
-                          zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫
-                     zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
-                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                     zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where
-                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
-                          zc13 (fsuc x fc) with zc13 fc
-                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-                          ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
-                          zc13 (init asu su=z ) with trio< u x
-                          ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫
-                          ... | tri≈ ¬a b ¬c = ?
-                          ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c )
-                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
-                 sup {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
-                 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))
-                 sis {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = {!!} where
-                     zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSUP A (UnionCF A f mf ay supf1 b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b
-                 sup=u {z} ab z≤x is-sup with trio< z x
-                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x≤sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x≤sup = {!!} }
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
+          sfpx≤spu : {z : Ordinal } → supf1 z o≤ spu
+          sfpx≤spu {z} = ? -- subst ( λ k → k o≤ spu) (sym (ZChain.supf-is-minsup zc o≤-refl ))  
+            -- ( MinSUP.minsup (ZChain.minsup zc o≤-refl) (MinSUP.asm supu)  
+            --  (λ {x} ux → MinSUP.x≤sup supu (case1 ux)) )
+
+          supf-mono : {x y : Ordinal } → x o≤  y → supf1 x o≤ supf1 y
+          supf-mono {x} {y} x≤y = ?
 
           zc5 : ZChain A f mf ay x
-          zc5 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain f x  )
-               -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension {!!}
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSUP A pchain f ax )
-          ... | case1 is-sup = ? -- record { supf = supf1  ; sup=u = {!!}
-               -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?)
-          ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
+          zc5 with zc43 x spu
+          zc5 | (case2 sp≤x ) =  ? where
+                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                     → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
+          zc5 | (case1 x<sp ) =  ? where
+                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                     → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function