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

changeset 818:80df9b356e2c

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 Wed, 17 Aug 2022 09:20:32 +0900
parents 26450ab6dd4e
children 89c4e8f06ce1
files src/zorn.agda
diffstat 1 files changed, 16 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 16 22:49:16 2022 +0900
+++ b/src/zorn.agda	Wed Aug 17 09:20:32 2022 +0900
@@ -702,10 +702,9 @@
                ax : odef A x
                is-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
 
-          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o≤ px ) → (z1≤x :  z1 o≤ x ) 
-               → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
-          UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
+          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o≤ px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
+          UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
               zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w
               zc60 (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 z0≤1 ) 
@@ -813,17 +812,25 @@
                  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
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = ? }
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = {!!} }
-                 ... | tri> ¬a ¬b px<b = {!!} where
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o<→≤ a) lt) } 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
+                 ... | tri> ¬a ¬b px<b = ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
+                     zcsup0 : supf1 b ≡ b
+                     zcsup0 with zc30 | trio< b px
+                     ... | refl | tri< a ¬b ¬c = ?
+                     ... | refl | tri≈ ¬a b ¬c = ?
+                     ... | refl | tri> ¬a ¬b c = refl
+                     zcsup : xSUP
+                     zcsup with zc30
+                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono ? ? ? ? ? (UnionCF⊆ o≤-refl ? lt)) } } 
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf1 b
-                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
-                 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl )
+                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc (o<→≤ a) )
+                 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } =  
                     ⟪ SUP.as sup1  , ch-is-sup b  o≤-refl zc31 (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl))  ⟫  
                          where