# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662408940 -32400
# Node ID 14bd0c9ad267b869540c527eeb076470830107f4
# Parent  2569ace27176757dd19d92659188d7f0cf23669e
csupf b is no good, because supf1 x is not in UnionCF x ( but UnionCD (supf x) )

diff -r 2569ace27176 -r 14bd0c9ad267 src/zorn.agda
--- a/src/zorn.agda	Tue Sep 06 04:38:39 2022 +0900
+++ b/src/zorn.agda	Tue Sep 06 05:15:40 2022 +0900
@@ -297,7 +297,7 @@
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
+      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y 
    supf-inject {x} {y} sx<sy with trio< x y
    ... | tri< a ¬b ¬c = a
@@ -323,24 +323,8 @@
             s<b = supf-inject ss<sb
             s≤<z : s o≤ z
             s≤<z = ordtrans s<b b≤z
-            zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
-            zc04 = csupf s≤<z 
             zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
-            zc05 with zc04
-            ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u≤x ) is-sup fc ⟫ where
-                zc06 : supf u ≡ u
-                zc06 = ChainP.supu=u is-sup
-                zc09 : u o≤ supf s  →  u o≤ b 
-                zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s)
-                ... | case1 su=ss = zc08 where
-                    zc07 : supf u o≤ supf b   
-                    zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono  (o<→≤ s<b)  )
-                    zc08 :  u o≤ b 
-                    zc08 with osuc-≡< zc07
-                    ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb )
-                    ... | case2 lt =  o<→≤ (supf-inject lt )
-                ... | case2 lt =  o<→≤ (ordtrans (supf-inject lt) s<b) 
+            zc05 = ? -- csupf s≤<z 
    csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
@@ -899,7 +883,7 @@
                      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 px) (supf1 px b)) (supf1 px b)
+                 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (supf1 px) b) (supf1 px b)
                  csupf {b} b≤x = zc05 where
                      zc04 : (b o≤ px ) ∨ (b ≡ x )
                      zc04 with trio< b px 
@@ -908,15 +892,15 @@
                      ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
                      ... | case1 eq = case2 eq
                      ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
-                     zc05 : odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b)
+                     zc05 : odef (UnionCF A f mf ay (supf1 px) b) (supf1 px b)
                      zc05 with zc04
                      ... | case2 b=x with ZChain.csupf zc o≤-refl
                      ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au  
                          , ch-init (subst₂ (λ j k → FClosure A f j k  ) refl (supfx b=x) fc) ⟫ 
                      ... | ⟪ au , ch-is-sup u u≤x is-sup fc  ⟫  = ⟪ subst (λ k → odef A k) (supfx b=x) au  
-                         , ch-is-sup u (subst (λ k → u o≤ k) (supfx b=x) u≤x) ? zc06 ⟫ where
+                         , ch-is-sup u ? ? zc06 ⟫ where
                            zc08 : supf0 u o≤ supf0 px
-                           zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x
+                           zc08 = ? -- subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x
                            zc06 : FClosure A f (supf1 px u)  (supf1 px b)
                            zc06 with osuc-≡< zc08
                            ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supfx b=x)  fc where
@@ -931,9 +915,9 @@
                      ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au  
                          , ch-init (subst₂ (λ j k → FClosure A f j k  ) refl (supf0=1 b≤px) fc) ⟫ 
                      ... | ⟪ au , ch-is-sup u u≤x is-sup fc  ⟫  = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au  
-                         , ch-is-sup u (subst (λ k → u o≤ k) (supf0=1 b≤px) u≤x) ? zc06 ⟫ where
+                         , ch-is-sup u (subst (λ k → u o≤ k) ? ? ) ? zc06 ⟫ where
                            zc08 : supf0 u o≤ supf0 b
-                           zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x
+                           zc08 = ? -- subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x
                            zc06 : FClosure A f (supf1 px u)  (supf1 px b)
                            zc06 with osuc-≡< zc08
                            ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supf0=1 b≤px)  fc where
@@ -1097,7 +1081,7 @@
                  ... | 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 )) 
-                 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 (supf1 z)) (supf1 z)
+                 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
                  csupf {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = ?  where
                      zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)