# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671249497 -32400
# Node ID 83d9000bf72f6a9936ac52097f905ad9a85c7f7e
# Parent  7089a047e49f79589d677611bbbfdf8e56c451ab
0< is no good

diff -r 7089a047e49f -r 83d9000bf72f src/zorn.agda
--- a/src/zorn.agda	Sat Dec 17 06:07:18 2022 +0900
+++ b/src/zorn.agda	Sat Dec 17 12:58:17 2022 +0900
@@ -1238,7 +1238,7 @@
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-     ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = 0<supfz
+     ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = 0<supfz (ysup f mf ay)
               ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
               ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0)))    } where
           mf : ≤-monotonic-f A f
@@ -1246,16 +1246,16 @@
              mf00 : * x < * (f x)
              mf00 = proj1 ( mf< x ax )
           ym = MinSUP.sup (ysup f mf ay)
-          0<supfz : o∅ o< MinSUP.sup (ysup f mf ay)
-          0<supfz with trio< o∅ (MinSUP.sup (ysup f mf ay) )
+          0<supfz : (ysup : MinSUP A (uchain f mf ay)) → o∅ o< MinSUP.sup ysup
+          0<supfz ysup with trio< o∅ (MinSUP.sup ysup )
           ... | tri< a ¬b ¬c = a
-          ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ ? (MinSUP.minsup (ysup f mf ay) (proj2 (mf _ (MinSUP.as (ysup f mf ay) )))  mf01 )) where
-                mf01 : {w : Ordinal} → odef (uchain f mf ay) w → w ≤ f (MinSUP.sup (ysup f mf ay))
-                mf01 {w} uw = ≤-ftrans (MinSUP.x≤sup (ysup f mf ay) uw) (proj1 (mf _ (MinSUP.as (ysup f mf ay) )))
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ ? (MinSUP.minsup ysup (proj2 (mf _ (MinSUP.as ysup  )))  mf01 )) where
+                mf01 : {w : Ordinal} → odef (uchain f mf ay) w → w ≤ f (MinSUP.sup ysup )
+                mf01 {w} uw = ≤-ftrans (MinSUP.x≤sup ysup uw) (proj1 (mf _ (MinSUP.as ysup  )))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0  c )
           zo≤sz : {z : Ordinal} → z o≤ x → z o≤ MinSUP.sup (ysup f mf ay)
           zo≤sz {z} z≤x with osuc-≡< z≤x
-          ... | case1 refl = o<→≤ (subst (λ k → k o< MinSUP.sup (ysup f mf ay)) (sym x=0) 0<supfz )
+          ... | case1 refl = o<→≤ (subst (λ k → k o< MinSUP.sup (ysup f mf ay)) (sym x=0) (0<supfz (ysup f mf ay) ) )
           ... | case2 lt = ⊥-elim ( ¬x<0  (subst (λ k → z o< k ) x=0 lt ) )
           is-minsup : {z : Ordinal} → z o≤ x →
             IsMinSUP A (UnionCF A f ay (λ _ → MinSUP.sup (ysup f mf ay)) z) (MinSUP.sup (ysup f mf ay))
@@ -1598,18 +1598,18 @@
                    zc44 : FClosure A f (supf1 u) w
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
-
           zo≤sz : {z : Ordinal} →  z o≤ x → z o≤ supf1 z
           zo≤sz {z} z≤x with osuc-≡< z≤x
           ... | case2 z<x = subst (λ k → z o≤ k) (sym (trans (sf1=sf z<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl)))) ( ZChain.zo≤sz (pzc z<x) o≤-refl )
-          ... | case1 refl = ? where -- subst (λ k → x o≤ k) (sf1=spu refl) ? where
+          ... | case1 refl = subst (λ k → x o≤ k) (sym (sf1=spu refl)) z47 where
                z47 : x o≤ spu
                z47 with x<y∨y≤x spu x
                ... | case2 lt = lt
                ... | case1 spu<x = ⊥-elim ( <<-irr (MinSUP.x≤sup usup z48) (proj1 ( mf< spu (MinSUP.as usup))))  where
                    z49 : supfz spu<x ≡ spu
                    z49 with trio< (supfz spu<x) spu
-                   ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup (o<→≤ spu<x)) (MinSUP.as usup) z51 ) ? ) where
+                   ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup (o<→≤ spu<x)) (MinSUP.as usup) z51 )
+                         (subst₂ (λ j k → j o< k ) refl (trans (zeq _ _ o≤-refl (o<→≤ <-osuc)) (sym (sf1=sf spu<x)))  c)) where
                        z51 : {w : Ordinal  } → odef (UnionCF A f ay supf1 spu)  w → w ≤ spu
                        z51 {w}  ⟪ aw , ch-init fc ⟫  = MinSUP.x≤sup usup  ⟪ aw , ic-init fc ⟫
                        z51 {w}  ⟪ aw , ch-is-sup u u<b su=u fc  ⟫  = MinSUP.x≤sup usup ⟪ aw , ic-isup u (ordtrans u<b spu<x) z55 z56 ⟫ where
@@ -1622,29 +1622,37 @@
                             z56 : FClosure A f (supfz (ordtrans u<b spu<x)) w
                             z56 = subst (λ k → FClosure A f k w ) (sym (trans (zeq _ _  o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<z)))) fc
                    ... | tri≈ ¬a b ¬c = b
-                   ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x)))  z52 ) ? ) where
+                   ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x)))  z52 )
+                         (subst₂ (λ j k → j  o< k) (zeq _ _ o≤-refl (o<→≤ <-osuc)) refl a)) where
                        z52 : {w : Ordinal  } → odef pchainU  w → w ≤ supfz spu<x
-                       z52 {w} uw = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) z53  ) where
+                       z52 {w} ⟪ aw , ic-init fc ⟫ = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) ⟪ aw , ch-init fc ⟫  )
+                       z52 {w} ⟪ aw , ic-isup u u<b sa<b fc ⟫ = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) z53  ) where
+                            --   sa<b  : supfz u<b o≤ u
+                            --   a : supfz spu<x o< spu
+                            z60 : odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim u<b))) (osuc u)) w
+                            z60 = ZChain.cfcs (pzc (ob<x lim u<b)) <-osuc o≤-refl sa<b fc
                             z53 : odef (UnionCF A f ay supf1 spu) w
-                            z53 with pchainU⊆chain uw
-                            ... |  ⟪ aw , ch-init fc ⟫  = ⟪ aw , ch-init fc ⟫
-                            ... |  ⟪ aw , ch-is-sup u u<b su=u fc  ⟫  = ⟪ aw , ch-is-sup u u<spu
-                                (trans (trans (sf1=sf u<z) (zeq _ _ z54 (o<→≤ <-osuc))) su=u )
-                                (subst (λ k → FClosure A f k w) (sym (trans (sf1=sf u<z) (zeq _ _ z54 (o<→≤ <-osuc))))  fc)  ⟫  where
-                               u<spu : u o< spu
-                               u<spu = ? -- ordtrans u<b (pic<x (proj2 uw))
-                               u<z : u o< z
-                               u<z = ordtrans u<spu spu<x
-                               z54 : osuc u o≤ osuc (IChain-i (proj2 uw))
-                               z54 = osucc u<b
-                                -- u<b : u o< osuc (IChain-i (proj2 uw))
-                   z50 : supfz spu<x o≤ x
-                   z50 = ? -- o<→≤ ( subst (λ k → k o< x) z49 ?) -- spu<x )
+                            z53 with z60
+                            ... | ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+                            ... | ⟪ aw , ch-is-sup u u<z su=u fc ⟫ = ⟪ aw , ch-is-sup u z54 z55 z56 ⟫ where
+                                 z54 : u o< spu
+                                 z54 = osucprev ( begin
+                                    osuc u ≡⟨ cong osuc (sym su=u)  ⟩
+                                    osuc (ZChain.supf (pzc (ob<x lim u<b)) u )  ≤⟨ ? ⟩
+                                    supfz spu<x <⟨ a ⟩
+                                    spu ∎ ) where open o≤-Reasoning O
+                                 z57 : supf1 u ≡  ZChain.supf (pzc (ob<x lim u<b)) u
+                                 z57 = trans (sf1=sf ?) (zeq _ _ ? ? )
+                                 z55 : supf1 u ≡ u
+                                 z55 = trans z57 su=u
+                                 z56 : FClosure A f (supf1 u) w
+                                 z56 = subst (λ k → FClosure A f k w) (sym z57) fc
+                   z50 : supfz spu<x o≤ spu
+                   z50 = o≤-refl0 z49
                    z48 : odef pchainU (f spu)
-                   z48 = ⟪  proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) ? -- z50
+                   z48 = ⟪  proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50
                         (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫
 
-
           supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
           supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
           ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
@@ -1681,8 +1689,8 @@
                a<b = supf-inject0 supf-mono sa<sb
                a<x : a o< x
                a<x = ordtrans<-≤ a<b b≤x
-          ... | case1 refl = ? where -- zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb)
-                   -- (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc ) where
+          ... | case1 refl = subst (λ k → w ≤ k ) (sym (sf1=spu refl)) (  zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb)
+                   (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc )) where
                a<x : a o< x
                a<x = supf-inject0 supf-mono sa<sb
                zc40 : ZChain.supf (pzc  (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc  (ob<x lim a<x )) a) w → w ≤ spu