# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662354281 -32400
# Node ID 2d8ce664ae31385f9069712a5ec225198c4acfa0
# Parent  f1f779930fbf543b020ed9ad4d5e590930d32fdb
...

diff -r f1f779930fbf -r 2d8ce664ae31 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sun Sep 04 14:25:01 2022 +0900
+++ b/src/OrdUtil.agda	Mon Sep 05 14:04:41 2022 +0900
@@ -70,6 +70,7 @@
 pxo≤x : {x : Ordinal} (op : Oprev Ordinal osuc x)  → Oprev.oprev op o< osuc x
 pxo≤x {x} op = ordtrans (pxo<x {x} op ) <-osuc
 
+
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
@@ -215,6 +216,14 @@
 ... | tri≈ ¬a b ¬c = ⊥-elim (not (o≤-refl0 (sym b)))
 ... | tri> ¬a ¬b c = ⊥-elim (not (o<→≤ c ))
 
+b≤px∨b=x : {b x  : Ordinal } → (op : Oprev Ordinal osuc x ) → b o≤ x  →   (b o≤ (Oprev.oprev op) ) ∨ (b ≡ x )
+b≤px∨b=x {b} {x} op b≤x with trio< b (Oprev.oprev op) 
+... | tri< a ¬b ¬c = case1 (o<→≤ a)
+... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
+... | 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  ⟫ ) 
+
 OrdTrans :  Transitive  _o≤_
 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
diff -r f1f779930fbf -r 2d8ce664ae31 src/zorn.agda
--- a/src/zorn.agda	Sun Sep 04 14:25:01 2022 +0900
+++ b/src/zorn.agda	Mon Sep 05 14:04:41 2022 +0900
@@ -738,14 +738,11 @@
 
           supf0 = ZChain.supf zc
 
-          sup1 : SUP A (UnionCF A f mf ay supf0 px)
-          sup1 = supP pchain pchain⊆A ptotal
-          sp1 = & (SUP.sup sup1 )
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z px
           ... | tri< a ¬b ¬c = ZChain.supf zc z
           ... | tri≈ ¬a b ¬c = ZChain.supf zc z
-          ... | tri> ¬a ¬b c = sp1 
+          ... | tri> ¬a ¬b c = ZChain.supf zc px
 
           pchain1 : HOD
           pchain1  = UnionCF A f mf ay supf1 x
@@ -774,17 +771,11 @@
           ... | tri≈ ¬a b ¬c = refl
           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
 
-          supf1=sp : {z : Ordinal } → x o≤ z  → supf1 z ≡ sp1
-          supf1=sp {z} x≤z with trio< z px
-          ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
-          ... | tri≈ ¬a refl ¬c = ⊥-elim ( o≤> x≤z (pxo<x op))
-          ... | tri> ¬a ¬b c = refl
-
           supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b)
-          supf∈A {b} b≤z = ?
-
-          supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1
-          supf1≤sp1 = ?
+          supf∈A {b} b≤z with trio< b px
+          ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a ))
+          ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b ))
+          ... | tri> ¬a ¬b c = proj1 ( ZChain.csupf zc o≤-refl )
 
           supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
           supf-mono = ?
@@ -848,112 +839,29 @@
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                      zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc12 fc where
-                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u1) z → odef pchain1 z
-                          zc12 (fsuc x fc) with zc12 fc
-                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
-                          ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
-                          zc12 (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 (o<→≤ px<x) ) 
-                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
-                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
-                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
-                              order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
-                                (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-                              ... | tri< a ¬b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
-                              ... | tri≈ ¬a b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) 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 = supf-inject0 supf-mono (subst₂ (λ j k → j o< k ) (sym eq2) refl s<u1 )
-                              ---   s ≡ sp1, px<s = px o< sp1
-                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x (o<→≤ px<x) ) 
-                            record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
-                              fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
-                              fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
-                              order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
-                                (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
-                              ... | tri< a ¬b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
-                              ... | tri≈ ¬a b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
-                              ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b zc14 ) ))  where --  px o< s < u1 = px 
-                                 zc14 :  s o< u1
-                                 zc14 = supf-inject0 supf-mono (subst₂ (λ j k → j o< k ) (sym eq2) refl s<u1 )
-                          ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x 
-                          ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
-                          ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
-
+                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 u1≤x u1-is-sup)  (fc0→1 u1≤x fc)  ⟫
                      zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
                      zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc13 fc where
-                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u1) z → odef pchain z
-                          zc13 (fsuc x fc) with zc13 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₁) ⟫ 
-                          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 (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 )) 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) ) 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 (¬sp=x zcsup)  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 )
+                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x
+                     ... | case1 eq = ⊥-elim (¬sp=x zcsup) where
+                             x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
+                             x<sup = ?
+                             zc12 : supf1 x ≡ u1
+                             zc12 = subst  (λ k → supf1 k ≡ u1) eq  (ChainP.supu=u u1-is-sup)
                              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 } }
-
+                             zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) ; is-sup = record { x<sup = x<sup } }
+                     ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 u1≤px u1-is-sup)  (fc1→0 u1≤px fc)  ⟫ where
+                                u1≤px : u1 o≤ px  
+                                u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt)
                  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} = SUP⊆ (UnionCF1⊆0 (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) 
                  ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) )
-                 ... | tri> ¬a ¬b px<z | record { eq = eq1} = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc31 } where
+                 ... | tri> ¬a ¬b px<z | record { eq = eq1} = ? where
                      zc30 : z ≡ x
                      zc30 with osuc-≡< z≤x
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
-                     zc31 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w  → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc31 {w} lt with zc30
-                     ... | refl = SUP.x<sup sup1 (subst (λ k → odef k (& w)) (sym pchain0=1) lt )
                  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 px
@@ -983,14 +891,12 @@
                      zc01 : odef A (supf1 b)
                      zc01 with zc04
                      ... | case1 le = proj1 ( csupf0 le )
-                     ... | case2 eq = subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1)
+                     ... | case2 eq = ? -- subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1)
                      u = supf1 b
                      supu=u : supf1 u ≡ u
                      supu=u with zc04
                      ... | case2 eq = begin
-                        supf1 u ≡⟨ cong supf1 (supf1=sp ? ) ⟩
-                        supf1 sp1 ≡⟨ supf1=sp ?  ⟩
-                        sp1 ≡⟨ sym (supf1=sp ?)  ⟩
+                        supf1 u ≡⟨ ? ⟩
                         u ∎ where open ≡-Reasoning
                      ... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? )  where
                          zc06 : b o≤ px