Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1080:11e869f92504

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Dec 2022 20:03:01 +0900
parents c2546206c891
children 7089a047e49f
files src/zorn.agda
diffstat 1 files changed, 26 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 16 17:00:44 2022 +0900
+++ b/src/zorn.agda	Fri Dec 16 20:03:01 2022 +0900
@@ -1589,7 +1589,32 @@
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
           zo≤sz : {z : Ordinal} →  z o≤ x → z o≤ supf1 z
-          zo≤sz = ?
+          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 = subst (λ k → x o≤ k) (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 ) a ) 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) ? ? ⟫
+                   ... | tri≈ ¬a b ¬c = b
+                   ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x)))  z52 ) c ) 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
+                            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 ? ? ?  ⟫
+                   z50 : supfz spu<x o≤ x
+                   z50 = o<→≤ ( subst (λ k → k o< x) z49 spu<x )
+                   z48 : odef pchainU (f spu)
+                   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)) ⟫
 
           order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
           order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x