# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662679190 -32400
# Node ID 269467244745edbd3774cb35085ba9d58d3d8eb3
# Parent  4e60b42b83a3791ff5ae04796b9622a881e95435
...

diff -r 4e60b42b83a3 -r 269467244745 src/zorn.agda
--- a/src/zorn.agda	Thu Sep 08 14:33:08 2022 +0900
+++ b/src/zorn.agda	Fri Sep 09 08:19:50 2022 +0900
@@ -882,22 +882,22 @@
           ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = supf1 
+                record {  supf = supf1 ; supf-max = ?
                    ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
                    ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supf1 : Ordinal → Ordinal
              supf1 z with trio< z px 
-             ... | tri< a ¬b ¬c = ZChain.supf zc z
-             ... | tri≈ ¬a b ¬c = ZChain.supf zc z
-             ... | tri> ¬a ¬b c = x
+             ... | tri< a ¬b ¬c = ZChain.supf zc z 
+             ... | tri≈ ¬a b ¬c = ZChain.supf zc z 
+             ... | tri> ¬a ¬b c = x --- SUP A (UnionCF A f mf ay supf0 px) ≡ SUP A (UnionCF A f mf ay supf1 px) 
 
              pchainx : HOD
              pchainx = UnionCF A f mf ay supf1 x
 
-             supf0px=x : supf0 px ≡ x
-             supf0px=x = ? where
+             supf0px=x : (ax : odef A x) → IsSup A (ZChain.chain zc ) ax → x ≡  & (SUP.sup (ZChain.sup zc o≤-refl ) )
+             supf0px=x is-sup = ? where
                  zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
-                 zc50 = ZChain.spuf-is-sup zc ?
+                 zc50 = ZChain.supf-is-sup zc ?
 
              supf-monox : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
              supf-monox {i} {j} i≤j with trio< i px | trio< j px
@@ -921,6 +921,15 @@
              ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
              ... | tri> ¬a ¬b c = refl
             
+             pchain0=x : UnionCF A f mf ay supf0 px ≡ UnionCF A f mf ay supf1 px 
+             pchain0=x =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
+                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → odef (UnionCF A f mf ay supf1 px) z
+                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ?  ⟫
+                     zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 px) z → OD.def (od pchain) z
+                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ?
+
              csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
              csupf {b} b≤x with zc04 b≤x 
              ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫