# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659665344 -32400
# Node ID 0acbc2b102e927baa35ea1c26bb968a8149dd70c
# Parent  bcc241fbb390f18ac70a54e10b4aefdf097577cd
...

diff -r bcc241fbb390 -r 0acbc2b102e9 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 05 09:22:47 2022 +0900
+++ b/src/zorn.agda	Fri Aug 05 11:09:04 2022 +0900
@@ -816,12 +816,13 @@
 
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
+          ysp =  & (SUP.sup (ysup f mf ay))
 
           psupf0 : (z : Ordinal) → Ordinal
           psupf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = & A -- Sup of FClosure A f y z ?
-          ... | tri> ¬a ¬b c = & A -- 
+          ... | tri≈ ¬a b ¬c = ysp 
+          ... | tri> ¬a ¬b c = ysp 
 
           pchain0 : HOD
           pchain0 = UnionCF A f mf ay psupf0 x
@@ -835,50 +836,13 @@
           usup = supP pchain0 (λ lt → proj1 lt) ptotal0
           spu = & (SUP.sup usup)
 
-          psupf : Ordinal → Ordinal
-          psupf z with trio< z x 
+          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 = spu              -- ^^ this z dependcy have to be removed
-          ... | tri> ¬a ¬b c = spu   ----  ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a)))
-
-          psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-          psupf<z {z} z<x with trio< z x
-          ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ )
-          ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x)
-          ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x)
-
-          psupf=x : spu ≡ psupf x
-          psupf=x = zc20 refl where
-              zc20 : {z : Ordinal } → z ≡ x → spu ≡ psupf x
-              zc20 {z} z=x with trio< z x | inspect psupf z
-              ... | tri< a ¬b ¬c | _ = ⊥-elim ( ¬b z=x)
-              ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
-              ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
+          ... | tri≈ ¬a b ¬c = spu 
+          ... | tri> ¬a ¬b c = spu
 
-          csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
-          csupf z with trio< z x | inspect psupf z
-          ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
-                ozc = pzc (osuc z) (ob<x lim z<x)
-                zc13 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) z (ZChain.supf ozc z)
-                zc13  = ZChain.csupf ozc (ordtrans o≤-refl <-osuc )
-                zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
-                zc12  = ?
-                zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 = ⟪ az , ch-is-sup z ? cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
-                      az : odef A ( ZChain.supf ozc z )
-                      az = proj1 zc12
-                      zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
-                      zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
-                      ... | case1 eq = case1 (trans eq (sym eq1) )
-                      ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
-                      cp1 : ChainP A f mf ay psupf z 
-                      cp1 = record {  fcy<sup = zc20   ; order = ?  ; supu=u = ?} 
-                     ---  u = supf u = supf z 
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? {!!} {!!} {!!} ⟫ where
-                sa = SUP.A∋maximal usup
-          ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
-
-          fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u)
+          fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ supf1 u) ∨ (w << supf1 u)
           fcy<sup {u} {w} u<x fc with trio< u x 
           ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
                uzc = pzc (osuc u) (ob<x lim a)
@@ -886,25 +850,25 @@
           ... | tri> ¬a ¬b c = ⊥-elim (¬a u<x)
 
           pchain : HOD
-          pchain = UnionCF A f mf ay psupf x
+          pchain = UnionCF A f mf ay supf1 x
 
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u ? is-sup (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-               zc7 : y <= psupf _
+               zc7 : y <= supf1 _
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay refl)    ⟫
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay psupf ( (proj2 ca)) ( (proj2 cb)) 
+               uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
 
           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) →
@@ -914,27 +878,25 @@
           ... | ⟪ 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 ? is-sup (fsuc _ fc))  ⟫ 
+                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
-          no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!} 
-               ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
+          no-extension : ¬ spu ≡ x → ZChain A f mf ay x
+          no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = {!!} 
+               ; supf-is-sup = ?
+               ; csupf = ? ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = ? } where
+                 UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay ? x 
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension -- ¬ A ∋ p, just skip
+          ... | no noax = no-extension ? -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension  
+          ... | case1 pr = no-extension ? 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = {!!} 
-              ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?) 
-             psupf1 : Ordinal → Ordinal
-             psupf1 z with trio< z x 
-             ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
-             ... | tri≈ ¬a b ¬c = x
-             ... | tri> ¬a ¬b c = x
-          ... | case2 ¬x=sup =  no-extension -- x is not f y' nor sup of former ZChain from y -- no extention
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = supf1  ; sup=u = {!!} 
+               ; supf-is-sup = ?
+               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = ? ; supf-mono = ? } 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
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay   z  } (λ x → ind f mf ay x   ) (& A)