# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670054235 -32400
# Node ID f12a9b4066a0f2668ac973f565f648d75fb0c0ad
# Parent  4b525726f2df264429b6122e4e54bc6eecc0451c
...

diff -r 4b525726f2df -r f12a9b4066a0 src/zorn.agda
--- a/src/zorn.agda	Sat Dec 03 11:48:47 2022 +0900
+++ b/src/zorn.agda	Sat Dec 03 16:57:15 2022 +0900
@@ -863,8 +863,7 @@
              m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) sfpx≤sp1
 
           zc41 : ZChain A f mf< ay x
-          zc41 with zc43 x sp1
-          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ?
+          zc41 =  record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
               ; supfmax = ? ; is-minsup = ? ;  cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
@@ -930,20 +929,20 @@
                  fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px →  FClosure A f (supf1 u) z
                  fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
 
-                 sfpx<x : supf0 px o< x
-                 sfpx<x with trio< (supf0 px) x
+                 sfpx<x : sp1 o≤ x → supf0 px o< x
+                 sfpx<x sp1≤x with trio< (supf0 px) x
                  ... | tri< a ¬b ¬c = a 
                  ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
                       -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
                       m12 : supf0 px ≡ sp1
                       m12 with osuc-≡< m13
                       ... | case1 eq = eq
-                      ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) 
+                      ... | case2 lt = ⊥-elim ( o≤> sp1≤x (subst (λ k → k o< sp1) spx=x lt )) 
                       m10 : f (supf0 px) ≡ supf0 px
                       m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where
                           m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1)
                           m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc)  
-                 ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
+                 ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp1≤x )))   -- x o< supf0 px o≤ sp1 ≤ x
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
@@ -1020,12 +1019,12 @@
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
                       csupf1 : odef (UnionCF A f ay supf1 b) w
-                      csupf1 = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫  where
+                      csupf1 = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) (sfpx<x ?)) z52 fc1 ⟫  where
                           spx = supf0 px
                           spx≤px : supf0 px o≤ px
-                          spx≤px = zc-b<x _ sfpx<x
+                          spx≤px = zc-b<x _ (sfpx<x ?)
                           z52 : supf1 (supf0 px) ≡ supf0 px
-                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ sfpx<x ) )
+                          z52 = trans (sf1=sf0 (zc-b<x _ (sfpx<x ?))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (sfpx<x ?) ) )
                           fc1 : FClosure A f (supf1 spx) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
@@ -1069,9 +1068,9 @@
                         z25 : {w : Ordinal } → odef pchainpx w → w ≤ s 
                         z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where
                             z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x o≤ 
-                            z28 = subst (λ k → supf0 px o< k) (sym z=x) sfpx<x
+                            z28 = subst (λ k → supf0 px o< k) (sym z=x) (sfpx<x ?)
                             z29 : supf0 px o≤ px 
-                            z29 = zc-b<x _ sfpx<x
+                            z29 = zc-b<x _ (sfpx<x ?)
                             z27 : supf1 (supf0 px) ≡ supf0 px
                             z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 )
                             fc1 : FClosure A f (supf1 (supf0 px)) w
@@ -1116,120 +1115,11 @@
                      zc22 : a o< osuc px
                      zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
 
-          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc ; order = ?
-              ; supfmax = ? ; sup=u = ? ; is-minsup = ? ; cfcs = cfcs    }  where
-
-                 --  supf0 px not is included by the chain
-                 --     supf1 x ≡ supf0 px because of supfmax
-
-                 cfcs : {a b w : Ordinal } → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f ay supf0 b) w
-                 cfcs {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
-                 ... | tri< a ¬b ¬c = ZChain.cfcs zc a<b (o<→≤ a) sa<b fc
-                 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc a<b o≤-refl sa<b fc 
-                 ... | tri> ¬a ¬b px<b = cfcs1 where
-                     x=b : x ≡ b
-                     x=b with trio< x b
-                     ... | tri< a ¬b ¬c = ⊥-elim ( o≤> b≤x a )
-                     ... | tri≈ ¬a b ¬c = b
-                     ... | tri> ¬a ¬b c = ⊥-elim (  ¬p<x<op ⟪ px<b , zc-b<x _ c ⟫  )  -- px o< b o< x
-                     --  a o< x, supf a o< x
-                     --      a o< px , supf a o< px → odef U w
-                     --      a ≡ px         -- supf0 px o< x → odef U w
-                     --      supf a ≡ px    -- a o< px → odef U w
-                     --                        a ≡ px → supf px ≡ px → odef U w
-
-                     cfcs0 : a ≡ px → odef (UnionCF A f ay supf0 b) w
-                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ? ⟫ where
-                         spx<b : supf0 px o< b
-                         spx<b = subst (λ k → supf0 k o< b) a=px sa<b
-                         cs01 : supf0 a ≡ supf0 (supf0 px)
-                         cs01 = trans (cong supf0 a=px) ( sym ( ZChain.supf-idem zc o≤-refl 
-                              (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
-                         fc1 : FClosure A f (supf0 (supf0 px)) w
-                         fc1 = subst (λ k → FClosure A f k w) cs01 fc
-                         m : MinSUP A (UnionCF A f ay supf0 (supf0 px))
-                         m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x))
-                         m=sa : MinSUP.sup m ≡ supf0 (supf0 px)
-                         m=sa = begin 
-                                MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x) ))  ⟩ 
-                                supf0 (supf0 px)  ∎  where open ≡-Reasoning 
-
-
-                     cfcs1 : odef (UnionCF A f ay supf0 b) w
-                     cfcs1 with trio< a px
-                     ... | tri< a<px ¬b ¬c = cfcs2 where
-                         sa<x : supf0 a o< x
-                         sa<x = ordtrans<-≤ sa<b b≤x
-                         cfcs2 : odef (UnionCF A f ay supf0 b) w
-                         cfcs2 with trio< (supf0 a) px
-                         ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
-                             ( ZChain.cfcs zc a<px o≤-refl sa<x fc ) 
-                         ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x)  ⟫ )
-                         ... | tri≈ ¬a sa=px ¬c with trio< a px
-                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ? ⟫ where
-                              cs01 : supf0 a ≡ supf0 (supf0 a)
-                              cs01 =  sym ( ZChain.supf-idem zc (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
-                              fc1 : FClosure A f (supf0 (supf0 a)) w
-                              fc1 = subst (λ k → FClosure A f k w) cs01 fc
-                              m : MinSUP A (UnionCF A f ay supf0 (supf0 a))
-                              m = ZChain.minsup zc (o≤-refl0 sa=px)
-                              m=sa : MinSUP.sup m ≡ supf0 (supf0 a)
-                              m=sa = begin 
-                                    MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (o≤-refl0 sa=px) )  ⟩ 
-                                    supf0 (supf0 a)  ∎  where open ≡-Reasoning 
-                         ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
-                         ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) )  ⟫ )
-                     ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
-                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (zc-b<x _ (ordtrans<-≤ a<b b≤x)) c )
-
-                 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
-                 zc17 {z} with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.supf-mono zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)
-                 ... | tri> ¬a ¬b px<z = o≤-refl0 zc177 where
-                      zc177 : supf0 z ≡ supf0 px
-                      zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
-
-                 zc11 : {z : Ordinal} → odef (UnionCF A f ay supf0 x) z → odef pchainpx z
-                 zc11 {z} ⟪ az , cp ⟫ = ? 
-
-                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
-                     field
-                         tsup : MinSUP A (UnionCF A f ay supf0 z)
-                         tsup=sup : supf0 z ≡ MinSUP.sup tsup
-
-                 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
-                 sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = record { tsup = ZChain.minsup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-minsup zc (o<→≤ a) }
-                 ... | tri≈ ¬a b ¬c = record { tsup = ZChain.minsup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-minsup zc (o≤-refl0 b) }
-                 ... | tri> ¬a ¬b px<z = zc35 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 ⟫ )
-                     zc32 = ?
-                     zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 ne {w} lt = ?
-                     zc33 : supf0 z ≡ & (SUP.sup zc32)
-                     zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
-                     zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
-                     zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.ax zc32 ; x≤sup = zc34 ne } ; tsup=sup = zc33  }
-                     zc35 : STMP z≤x
-                     zc35 with trio< (supf0 px) px
-                     ... | tri< a ¬b ¬c = zc36 ¬b
-                     ... | tri> ¬a ¬b c = zc36 ¬b
-                     ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
-                          zc37 : MinSUP A (UnionCF A f ay supf0 z)
-                          zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? }
-
-                 is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
-                 is-minsup = ?
-
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsMinSUP A (UnionCF A f ay supf0 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf0 b) f b ) → supf0 b ≡ b
+                    b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → 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) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , ? ⟫
+                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup
+                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) is-sup
                  ... | tri> ¬a ¬b px<b = ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x