# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661951313 -32400
# Node ID ef7c721b32dc8a0064a145cd40c6da0752cb47b0
# Parent  0855fce6ee9249cfbbf6bbf09c405f057b17b70c
csupf in not come from ZChain itself

diff -r 0855fce6ee92 -r ef7c721b32dc src/zorn.agda
--- a/src/zorn.agda	Wed Aug 31 19:48:12 2022 +0900
+++ b/src/zorn.agda	Wed Aug 31 22:08:33 2022 +0900
@@ -308,6 +308,16 @@
 
    -- ordering is proved here for totality and sup
 
+   supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
+   supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
+
+   csupf0 :  {b : Ordinal} → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b)
+   csupf0 {b} b≤z = ⟪ supf∈A b≤z  , ch-is-sup (supf b) o≤-refl  ? (init zc10 zc11 ) ⟫ where
+       zc11 : supf (supf b) ≡ supf b
+       zc11 = ?
+       zc10 : odef A (supf (supf b))
+       zc10 = subst (λ k → odef A k ) (sym zc11) (  supf∈A b≤z )
+
    fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ 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 ) ⟫ 
@@ -940,31 +950,24 @@
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc31 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w  → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc31 = ?
+                     zc31 {w} lt with zc30
+                     ... | refl = SUP.x<sup sup1 (subst (λ k → odef k (& w)) (sym pchain0=1) lt )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 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 is-sup ? } 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup ? } 
-                 ... | tri> ¬a ¬b px<b = ? where -- ⊥-elim (¬sp=x zcsup ) where
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o<→≤ a) lt) } 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o≤-refl0 b) lt) } 
+                 ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
                      ... | 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 ⟫ )
-                     zcsup : ?
-                     zcsup = ? -- with zc30
-                     -- ... | refl = case1 record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup ? } } 
+                     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 is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
                  csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
-                 csupf {b} b≤x with trio< b px | inspect supf0 b
-                 ... | tri< a ¬b ¬c | _ =  ? where
-                     zc31 = ZChain.csupf zc (o<→≤ a )
-                 ... | tri≈ ¬a refl ¬c | _ = ? where
-                     zc32 = ZChain.csupf zc o≤-refl 
-                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? where
-                     zc30 : x ≡ b
-                     zc30 with osuc-≡< b≤x
-                     ... | 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 ⟫ )
+                 csupf {b} b≤x = ?
                  sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
                  sis {z} z≤x  = zc40 where
                       zc40 : supf1 z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error