# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670891471 -32400
# Node ID 99df080f4fdb3d72c23d95f1a36acb9c6876c8bf
# Parent  f24f4de4d459f57dd1edb14a17ad9937bcc12c05
...

diff -r f24f4de4d459 -r 99df080f4fdb src/zorn.agda
--- a/src/zorn.agda	Tue Dec 13 02:59:01 2022 +0900
+++ b/src/zorn.agda	Tue Dec 13 09:31:11 2022 +0900
@@ -1249,9 +1249,6 @@
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ?
               ; zo≤sz = ?   ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
-          -- mf : ≤-monotonic-f A f
-          -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust
-
           mf : ≤-monotonic-f A f
           mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
              mf00 : * x < * (f x)
@@ -1265,8 +1262,8 @@
           supfz : {z : Ordinal } → z o< x → Ordinal
           supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
 
-          pchainx : HOD
-          pchainx = UnionIC A f ay supfz 
+          pchainU : HOD
+          pchainU = UnionIC A f ay supfz 
 
           zeq : {xa xb z : Ordinal }
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
@@ -1285,17 +1282,17 @@
           pic<x {z} (ic-init fc) = ob<x lim 0<x   -- 0<x ∧ lim x → osuc o∅ o< x
           pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x 
 
-          pchainx⊆chain : {z : Ordinal } → (pz : odef pchainx z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
-          pchainx⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
-          pchainx⊆chain {z} ⟪ aw , (ic-isup ia ia<x sa<x fca) ⟫ = ZChain.cfcs (pzc (ob<x lim ia<x) ) <-osuc o≤-refl uz03 fca where
+          pchainU⊆chain : {z : Ordinal } → (pz : odef pchainU z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
+          pchainU⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+          pchainU⊆chain {z} ⟪ aw , (ic-isup ia ia<x sa<x fca) ⟫ = ZChain.cfcs (pzc (ob<x lim ia<x) ) <-osuc o≤-refl uz03 fca where
                uz02 : FClosure A f (ZChain.supf (pzc (ob<x lim ia<x)) ia ) z
                uz02 = fca
                uz03 : ZChain.supf (pzc (ob<x lim ia<x)) ia o≤ ia
                uz03 = sa<x
 
-          chain⊆pchainx : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainx w 
-          chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
-          chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ 
+          chain⊆pchainU : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainU w 
+          chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
+          chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ 
              = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ  k → FClosure A f k w ) su=su fc) ⟫ where
                  u<x : u o< x
                  u<x = ordtrans u<oz oz<x
@@ -1333,31 +1330,71 @@
               = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x)
                   (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc )
 
-          ptotalx : IsTotalOrderSet pchainx
-          ptotalx {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
-          ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainx⊆chain ib) 
-          ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainx⊆chain ib) 
-          ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
+          ptotalU : IsTotalOrderSet pchainU
+          ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
+          ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib) 
+          ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib) 
+          ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
+
+          usup : MinSUP A pchainU
+          usup = minsupP pchainU (λ ic → proj1 ic ) ptotalU
+          spu = MinSUP.sup usup
+
+
+          pchainS : HOD
+          pchainS = record { od = record { def = λ z →  (odef A z  ∧ IChain  ay supfz z )
+                ∨ (FClosure A f spu z ∧ (spu o< x)) } ; odmax = & A ; <odmax = zc00 } where
+               zc00 : {z : Ordinal } → (odef A z ∧ IChain ay supfz z ) ∨ (FClosure A f spu z ∧ (spu o< x) )→ z o< & A
+               zc00 {z} (case1 lt) = z07 lt
+               zc00 {z} (case2 fc) = z09 ( A∋fc spu f mf (proj1 fc) )
+
+          zc02 : { a b : Ordinal } → odef A a ∧ IChain ay supfz a → FClosure A f spu b ∧ ( spu o< x) → a ≤ b
+          zc02 {a} {b} ca fb = zc05 (proj1 fb) where
+             zc05 : {b : Ordinal } → FClosure A f spu b → a ≤ b
+             zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc spu f mf fb ))
+             ... | case1 eq = subst (λ k → a ≤ k ) eq (zc05 fb)
+             ... | case2 lt = ≤-ftrans (zc05 fb) (case2 lt)
+             zc05 (init b1 refl) = MinSUP.x≤sup usup ca
 
-          usup : MinSUP A pchainx
-          usup = minsupP pchainx (λ ic → ? ) ptotalx
-          spu = MinSUP.sup usup
+          ptotalS : IsTotalOrderSet pchainS
+          ptotalS (case1 a) (case1 b) =  ptotalU a b
+          ptotalS {a0} {b0} (case1 a) (case2 b) with zc02 a b
+          ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
+               eq1 : a0 ≡ b0
+               eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+          ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
+               lt1 : a0 < b0
+               lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+          ptotalS {b0} {a0} (case2 b) (case1 a) with zc02 a b
+          ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
+               eq1 : a0 ≡ b0
+               eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+          ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
+               lt1 : a0 < b0
+               lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+          ptotalS (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp spu f mf (proj1 a) (proj1 b))
+
+          S⊆A : pchainS ⊆' A
+          S⊆A (case1 lt) = proj1 lt
+          S⊆A (case2 fc) = A∋fc _ f mf (proj1 fc)
+
+          ssup : MinSUP A pchainS
+          ssup = minsupP pchainS S⊆A ptotalS
+
+          sps = MinSUP.sup ssup
 
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = spu
-          ... | tri> ¬a ¬b c = spu
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z   -- each sup o< x
+          ... | tri≈ ¬a b ¬c = spu                                 -- sup of all sup o< x
+          ... | tri> ¬a ¬b c = sps                                 -- sup of spu which o< x 
+                                                --  if x o< spu, spu is not included in UnionCF x
+          -- the chain
 
           pchain : HOD
           pchain = UnionCF A f ay supf1 x
 
-          -- pchain ⊆ pchainx
-
-          ptotal : IsTotalOrderSet pchain
-          ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = ? --  chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
+          -- pchain ⊆ pchainU ⊆ pchianS
 
           sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z
           sf1=sf {z} z<x with trio< z x
@@ -1365,22 +1402,28 @@
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
           ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
 
-          sf1=spu : {z : Ordinal } → (a : x o≤ z ) → supf1 z ≡ spu
-          sf1=spu {z} x≤z with trio< z x
+          sf1=spu : {z : Ordinal } → (a : x o≤ z ) → spu o< x → supf1 z ≡ spu
+          sf1=spu {z} x≤z s<x with trio< z x
           ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a)
           ... | tri≈ ¬a b ¬c = refl
-          ... | tri> ¬a ¬b c = refl
+          ... | tri> ¬a ¬b c = ?
 
-          zc11 : {z : Ordinal } → odef pchain z → odef pchainx z
+          sf1=sps : {z : Ordinal } → (a : x o≤ z ) → x o≤ spu → supf1 z ≡ sps
+          sf1=sps {z} x≤z x≤s with trio< z x
+          ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a)
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
+
+          zc11 : {z : Ordinal } → odef pchain z → odef pchainS z
           zc11 {z} lt = ?
 
-          sfpx≤spu : {z : Ordinal } → supf1 z ≤ spu
+          sfpx≤spu : {z : Ordinal } → supf1 z ≤ sps
           sfpx≤spu {z} with trio< z x
-          ... | tri< a ¬b ¬c = MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
-          ... | tri≈ ¬a b ¬c = case1 refl
-          ... | tri> ¬a ¬b c = case1 refl
+          ... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
+          ... | tri≈ ¬a b ¬c = case1 ?
+          ... | tri> ¬a ¬b c = case1 ?
 
-          sfpxo≤spu : {z : Ordinal } → supf1 z o≤ spu
+          sfpxo≤spu : {z : Ordinal } → supf1 z o≤ sps
           sfpxo≤spu {z} with trio< z x
           ... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
           ... | tri≈ ¬a b ¬c = o≤-refl0 ?
@@ -1390,13 +1433,13 @@
           asupf {z} with trio< z x
           ... | tri< a ¬b ¬c = ZChain.asupf (pzc  (ob<x lim a)) 
           ... | tri≈ ¬a b ¬c = MinSUP.as usup
-          ... | tri> ¬a ¬b c = MinSUP.as usup
+          ... | tri> ¬a ¬b c = MinSUP.as ssup
 
           supfmax : {z : Ordinal } → x o< z → supf1 z ≡ supf1 x
           supfmax {z} x<z with trio< z x
           ... | tri< a ¬b ¬c = ⊥-elim (o<> a x<z)
           ... | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (sym b) x<z)
-          ... | tri> ¬a ¬b c = sym (sf1=spu o≤-refl)
+          ... | tri> ¬a ¬b c = sym ? -- (sf1=sps o≤-refl)
 
           supf-mono : {z y : Ordinal } → z o≤ y → supf1 z o≤ supf1 y
           supf-mono {z} {y} z≤y with trio< y x
@@ -1501,7 +1544,7 @@
                ... | case1 eq = ⊥-elim ( ne eq )
                ... | case2 lt = lt
                z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp
-               z19 = record { ax = ? ;   x≤sup = z20 }  where
+               z19 = record { ax = asp ;   x≤sup = z20 }  where
                    z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
                    z20 {y} zy with MinSUP.x≤sup sp1
                        (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))