# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660554147 -32400
# Node ID 81018623e3c51b4e6680d420bca178037c734f87
# Parent  2141154c521bec6920f9585ab9159047a5e2dff1
...

diff -r 2141154c521b -r 81018623e3c5 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 12 15:16:50 2022 +0900
+++ b/src/zorn.agda	Mon Aug 15 18:02:27 2022 +0900
@@ -702,40 +702,55 @@
                ax : odef A x
                not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
 
-          UnionCF⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf0 u ⊆' UnionCF A f mf ay supf1 x 
-          UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
-          UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
-                  UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
-          ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
-          ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-          UnionCFR⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay supf0 x 
-          UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
-          UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
-                  UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
-          ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
-          ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z1≤x :  z1 o≤ x ) 
+               → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
+          UnionCF⊆ {z0} {z1} z0≤1 z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF⊆ {z0} {z1} z0≤1 z1≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
+              zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w
+              zc60 (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 (OrdTrans u1≤x z0≤1 ) 
+                record { fcy<sup = ? ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫
+              ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
+                record { fcy<sup = ? ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫
+              ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } = ? where
+                 zc31 : supf0 u1 ≡ u1
+                 zc31 = ChainP.supu=u u1-is-sup
+                 zc32 : u1 o≤ x
+                 zc32 = OrdTrans u1≤x (OrdTrans z0≤1 z1≤x )
+                 zc30 : x ≡ u1
+                 zc30 with osuc-≡< zc32
+                 ... | case1 eq = sym (eq)
+                 ... | case2 u1<x = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op)) u1<x ⟫ )
+              zc60 (fsuc w1 fc) with zc60 fc
+              ... | ⟪ 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₁) ⟫ 
           no-extension : ¬ xSUP → ZChain A f mf ay x
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
                ; 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 = ? }  where
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
+                 UnionCFR⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay supf0 x 
+                 UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫
+                 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with
+--                         UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+--                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+--                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
                  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 = SUP⊆ (UnionCFR⊆ ?) ( ZChain.sup zc (o<→≤ a) )
-                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ ?) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
-                 ... | tri> ¬a ¬b c = ?
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ {!!}) ( ZChain.sup zc (o<→≤ a) )
+                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ {!!}) ( 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 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) ?
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) ?
-                 ... | tri> ¬a ¬b c = ?
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) {!!}
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) {!!}
+                 ... | tri> ¬a ¬b c = {!!}
                  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 = UnionCF⊆ o≤-refl ( ZChain.csupf zc (o<→≤ a) )
-                 ... | tri≈ ¬a b ¬c = UnionCF⊆ o≤-refl ( ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
-                 ... | tri> ¬a ¬b px<b =  ⟪ ? , ch-is-sup b  o≤-refl ? ? ⟫  where
+                 ... | tri< a ¬b ¬c = UnionCF⊆ ? ? ( ZChain.csupf zc (o<→≤ a) )
+                 ... | tri≈ ¬a b ¬c = UnionCF⊆ ? ? ( ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
+                 ... | tri> ¬a ¬b px<b =  ⟪ {!!} , ch-is-sup b  o≤-refl {!!} {!!} ⟫  where
                      --   px< b ≤ x
                      -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
                      zc30 : x ≡ b
@@ -743,7 +758,7 @@
                      ... | 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) → supf1 z ≡ & (SUP.sup (sup z≤x))
-                 sis = ?
+                 sis = {!!}
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
@@ -767,12 +782,12 @@
              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 } = ⟪ ? , ? ⟫
-             ... | tri> ¬a ¬b c | record { eq = eq1 } = ? where -- b ≡ x, supf x ≡ sp
+             ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫
+             ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} where -- b ≡ x, supf x ≡ sp
                   zc30 : x ≡ b
                   zc30 with trio< x b
                   ... | tri< a ¬b ¬c = ?
-                  ... | tri≈ ¬a b ¬c = b
+                  ... | tri≈ ¬a b ¬c = ?
                   ... | tri> ¬a ¬b c = ?
 
           ... | case2 ¬x=sup =  no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention
@@ -856,23 +871,23 @@
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x 
                  UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
-                 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
-                      UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
-                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
-                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+                 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫
+                 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with
+--                      UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+--                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+--                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
                  UnionCF0⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay psupf0 x 
                  UnionCF0⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
-                 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
-                      UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
-                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
-                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+                 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫
+                 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with
+--                      UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+--                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+--                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) ?) ? )
-                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF0⊆ ?) usup
-                 ... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ ?) usup
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} )
+                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF0⊆ {!!}) usup
+                 ... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ {!!}) usup
                  sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z))
                  sis {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where
@@ -883,7 +898,7 @@
                  ... | case2 lt = ⊥-elim ( ¬a lt )
                  sup=u : {b : Ordinal} (ab : odef A 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 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 b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
                  csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
@@ -893,7 +908,7 @@
                      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 )
-                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x)) 
 
           zc5 : ZChain A f mf ay x 
@@ -905,7 +920,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = supf1  ; sup=u = {!!} 
                ; sup = {!!} ; supf-is-sup = {!!}
-               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = {!!}  } where -- x is a sup of (zc ?) 
+               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)