# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660714353 -32400
# Node ID 89c4e8f06ce183035e03eaaff61afe3a9cf91191
# Parent  80df9b356e2cf641c2f60ed15107f53c1a67bc8e
xSUP on px

diff -r 80df9b356e2c -r 89c4e8f06ce1 src/zorn.agda
--- a/src/zorn.agda	Wed Aug 17 09:20:32 2022 +0900
+++ b/src/zorn.agda	Wed Aug 17 14:32:33 2022 +0900
@@ -286,7 +286,7 @@
       sup : {x : Ordinal } → x o< z  → SUP A (UnionCF A f mf ay supf x)
       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) )
-      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
+      csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) 
 
    -- ordering is proved here for totality and sup
 
@@ -303,7 +303,7 @@
             s<z : s o< z
             s<z = ordtrans s<b b<z
             zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
-            zc03 with csupf (o<→≤ s<z )
+            zc03 with csupf s<z 
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ 
       zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
@@ -700,7 +700,7 @@
           record xSUP : Set n where
             field
                ax : odef A x
-               is-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
+               is-sup : IsSup A (UnionCF A f mf ay supf0 px) ax
 
           UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o≤ px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
           UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
@@ -789,8 +789,8 @@
                            supf1 u1 ≡⟨ zc33 ⟩
                            u1 ≡⟨ sym zc31 ⟩
                            x ∎ where open ≡-Reasoning
-                         zc34 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) z → (z ≡ x) ∨ (z << x)
-                         zc34 {z} lt with SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 x) k ) (sym &iso) lt )
+                         zc34 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 px) z → (z ≡ x) ∨ (z << x)
+                         zc34 {z} lt with SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 x) k ) (sym &iso) (chain-mono f mf ay supf0 (pxo≤x op) lt ) )
                          ... | case1 eq = case1 ( begin
                            z ≡⟨ sym &iso ⟩
                            & (* z) ≡⟨ cong (&) eq ⟩
@@ -814,32 +814,27 @@
                  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 (UnionCF⊆ o≤-refl (o<→≤ a) lt) } 
                  ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
-                 ... | tri> ¬a ¬b px<b = ? where
+                 ... | 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 ⟫ )
-                     zcsup0 : supf1 b ≡ b
-                     zcsup0 with zc30 | trio< b px
-                     ... | refl | tri< a ¬b ¬c = ?
-                     ... | refl | tri≈ ¬a b ¬c = ?
-                     ... | refl | tri> ¬a ¬b c = refl
                      zcsup : xSUP
                      zcsup with zc30
-                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono ? ? ? ? ? (UnionCF⊆ o≤-refl ? lt)) } } 
-                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
+                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) o≤-refl lt) } } 
+                 csupf : {b : Ordinal} → b o< x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf1 b
-                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc (o<→≤ a) )
-                 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
+                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc a  )
+                 ... | tri≈ ¬a b ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc ? )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } =  
-                    ⟪ SUP.as sup1  , ch-is-sup b  o≤-refl zc31 (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl))  ⟫  
+                    ⟪ SUP.as sup1  , ch-is-sup ?  ? ? (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl))  ⟫  
                          where
                      --   px< b ≤ x
                      -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
                      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 ⟫ )
+                     zc30 = ? -- with osuc-≡< ?
+                     -- ... | 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 ⟫ )
                      zc31 : ChainP A f mf ay supf1 b
                      zc31 = record { fcy<sup = {!!} ; order = {!!} ; supu=u = {!!} }
                  sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))
@@ -864,7 +859,7 @@
              ... | tri< a ¬b ¬c = ZChain.supf zc z
              ... | tri≈ ¬a b ¬c = x
              ... | tri> ¬a ¬b c = x
-             csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
+             csupf : {b : Ordinal} → b o< x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
              csupf {b} b≤x with trio< b px | inspect psupf1 b
              ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
              ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
@@ -984,15 +979,15 @@
                  ... | 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 c = {!!}
-                 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay 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 = zc9 where
                      zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
                      zc9 = {!!}
                      zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
-                     zc8 = ZChain.csupf  (pzc (osuc z) (ob<x lim a)) (o<→≤ <-osuc )
+                     zc8 = ZChain.csupf  (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc )
                  ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x)) 
+                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z ? )) 
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)