# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661837436 -32400
# Node ID ef0433f41e5562186ac7121ec37de73ab7c04529
# Parent  962a9f3dbd3c6c9e224b2790b322415989170101
...

diff -r 962a9f3dbd3c -r ef0433f41e55 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 30 09:49:25 2022 +0900
+++ b/src/zorn.agda	Tue Aug 30 14:30:36 2022 +0900
@@ -765,6 +765,12 @@
           pcy1 : odef pchain1 y
           pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
 
+          supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1
+          supf1≤sp1 = ?
+
+          supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
+          supf-mono = ?
+
           -- zc100  : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1
           -- zc100  = ?
 
@@ -776,8 +782,6 @@
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = supf-mono
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
-                 supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
-                 supf-mono = ?
                  pchain0=1 : pchain ≡ pchain1
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
@@ -825,27 +829,57 @@
                           ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                           ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
                           zc13 (init asp refl ) with trio< u1 px | inspect supf1 u1
-                          ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (subst (λ k → u1 o< k ) ? a )
-                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans ? (ChainP.supu=u u1-is-sup)   } (init ? ?)  ⟫ where
+                          ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (o<→≤ a)
+                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init (A∋fcs _ f mf fc) refl)  ⟫ where
                               fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
-                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
+                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
+                              order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 →
+                                (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
+                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
+                              ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) (sym eq2) (sym eq1) s<u1) (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) (sym eq2) (sym eq1) s<u1) (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans zc14 a ))) where --  px o< s < u1 < px
+                                 zc14 :  s o< u1
+                                 zc14 = ZChain.supf-inject zc s<u1 
+                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (o≤-refl0 b) 
+                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init (A∋fcs _ f mf fc)  refl )  ⟫ where
+                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
+                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
                               order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 →
                                 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
                               order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-                              ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                              ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                              ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? ))  --  px o< s < u1 < px
-                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x ? ) 
-                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ?) (ChainP.supu=u u1-is-sup)   } (init ? ? )  ⟫ where
-                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
-                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
-                              order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 →
-                                (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
-                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-                              ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                              ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
-                              ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? ))  --  px o< s < u1 = px
-                          ... | tri> ¬a ¬b c | _ = ⊥-elim ( o≤> u1≤x ? )
+                              ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) (sym eq2) (sym eq1) s<u1) (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) (sym eq2) (sym eq1) s<u1) (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
+                              ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k ) b zc14)))  where --  px o< s < u1 = px
+                                 zc14 :  s o< u1
+                                 zc14 = ZChain.supf-inject zc s<u1 
+                          ... | tri> ¬a ¬b px<u1 | record { eq = eq2 } = ⊥-elim ? where
+                             zc31 : x ≡ u1 
+                             zc31 with trio< x u1 
+                             ... | tri≈ ¬a b ¬c = b
+                             ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) c ⟫ )
+                             zc31 | tri< a ¬b ¬c with osuc-≡< (subst (λ k → u1 o≤ k ) refl u1≤x ) -- px<u1 u1≤x,
+                             ... | case1 u1=x = ⊥-elim ( ¬b (sym u1=x) )
+                             ... | case2 u1<x = ⊥-elim ( o<> u1<x a )
+                             zc33 : supf1 u1 ≡ u1   -- u1 ≡ supf1 u1 ≡ supf1 x ≡ sp1
+                             zc33 = ChainP.supu=u u1-is-sup
+                             zc32 : sp1 ≡ x 
+                             zc32 = begin
+                               sp1 ≡⟨ sym eq2 ⟩
+                               supf1 u1 ≡⟨ zc33 ⟩
+                               u1 ≡⟨ sym zc31 ⟩
+                               x ∎ where open ≡-Reasoning
+                             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 px) k ) (sym &iso) lt )
+                             ... | case1 eq = case1 ( begin
+                               z ≡⟨ sym &iso ⟩
+                               & (* z) ≡⟨ cong (&) eq ⟩
+                               sp1 ≡⟨ zc32 ⟩
+                               x ∎ ) where open ≡-Reasoning
+                             ... | case2 lt = case2 ( subst (λ k → * z < k ) (trans (sym *iso) (cong (*) zc32 )) lt )
+                             zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
+                             zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = zc34 } }
+
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px | inspect supf1 z
                  ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤   a) 
@@ -992,7 +1026,7 @@
           no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
                ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!}
-               ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
+               ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  pchain0=1 : pchain ≡ pchain1
@@ -1020,19 +1054,19 @@
                  sup {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )
                  ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b c = {!!}
+                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
                  sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))
-                 sis {z} z<x with trio< z x
+                 sis {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where
                      zc8 = ZChain.supf-is-sup (pzc z a) {!!}
                  ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b c = {!!}
+                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
                  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 x
+                 sup=u {z} ab z≤x is-sup with trio< z x
                  ... | 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)
+                 ... | 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} 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)
@@ -1040,7 +1074,7 @@
                      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 )
                  ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z {!!} )) 
+                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)