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

changeset 999:3ffbdd53d1ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fcs<sup requires <-monotonicity
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Nov 2022 09:41:13 +0900
parents e5f46d08c074
children 71f231c9ed6f
files src/zorn.agda
diffstat 1 files changed, 12 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Nov 17 19:04:06 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 09:41:13 2022 +0900
@@ -1029,6 +1029,8 @@
                  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
 
+                 -- this is a kind of maximality, so we cannot prove this without <-monotonicity
+                 --
                  fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
                  fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
@@ -1062,7 +1064,8 @@
                                    (sym (sf=eq u<x)) s<u)  
                                     (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
                                ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
-                 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b cp1 z51 ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 
+                 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b cp1 ? ⟫ where 
+                      -- a ≡ px , b ≡ x, sp o≤ x → supf px o< x 
                       px<b : px o< b
                       px<b = subst₂ (λ j k → j o< k) a=px refl a<b
                       b=x : b ≡ x
@@ -1072,6 +1075,14 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
                       z51 : FClosure A f (supf1 px) w
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
+                      -- what happens if supf0 px ≡ x ?    supf0 px ≡ sp ≡ x
+                      --     this does not happen in <-monotonic case
+                      csupf1 : odef (UnionCF A f mf ay supf1 x) (supf0 px)
+                      csupf1 = ⟪ ?  , ch-is-sup (supf0 px) z52 ? (init ? ? ) ⟫ where
+                          z52 : supf0 px o< x
+                          z52 = ?
+                      -- cspx : odef (UnionCF A f mf ay supf0 px) (supf0 px)
+                      -- cspx = ZChain.csupf zc ?
                       spx=px : supf1 px ≡ px
                       spx=px = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc (subst (λ k → odef A k) ? ?)  o≤-refl ? )
                       cp1 : ChainP A f mf ay supf1 px