# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660276575 -32400
# Node ID 473825abd7673604d906b3fdc147c74ef755f59d
# Parent  9d97134d0a9351740cdd2ec1a440e1d7510cbbd6
...

diff -r 9d97134d0a93 -r 473825abd767 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 12 09:02:51 2022 +0900
+++ b/src/zorn.agda	Fri Aug 12 12:56:15 2022 +0900
@@ -699,24 +699,24 @@
                not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
 
           no-extension : ¬ xSUP → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf0 ;  sup = sup
-               ; initial = pinit ; chain∋init = pcy ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
-              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext ;  f-total = ptotal }  where
-                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf0 z)
+          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
+               ; initial = ? ; chain∋init = ? ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = ? ;  f-total = ? }  where
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.sup zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
-                 ... | tri> ¬a ¬b c = ZChain.sup zc ?
+                 ... | tri< a ¬b ¬c = ? -- ZChain.sup zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
+                 ... | tri> ¬a ¬b c = ?
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf0 (osuc b)) ab → supf0 b ≡ b
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc 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) is-sup
-                 ... | tri≈ ¬a b ¬c =  ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) is-sup
+                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup
+                 ... | tri≈ ¬a b ¬c = ? --  ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) is-sup
                  ... | tri> ¬a ¬b c = ?
-                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 b) (supf0 b)
+                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px 
-                 ... | tri< a ¬b ¬c =  ZChain.csupf zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c =  ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
+                 ... | tri< a ¬b ¬c = ? --  ZChain.csupf zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = ? --  ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
                  ... | tri> ¬a ¬b px<b =  ? where
                      --   px< b ≤ x
                      -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
@@ -724,7 +724,7 @@
                      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 ⟫ )
-                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf0 z ≡ & (SUP.sup (sup z≤x))
+                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
                  sis = ?
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)