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

changeset 809:ab5aa49abde0

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 Mon, 15 Aug 2022 20:14:35 +0900
parents 81018623e3c5
children ae0f958e648b
files src/zorn.agda
diffstat 1 files changed, 20 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Aug 15 18:02:27 2022 +0900
+++ b/src/zorn.agda	Mon Aug 15 20:14:35 2022 +0900
@@ -702,25 +702,29 @@
                ax : odef A x
                not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
 
-          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z1≤x :  z1 o≤ x ) 
+          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 z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF⊆ {z0} {z1} z0≤1 z1≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
+          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
               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 ) 
-                record { fcy<sup = ? ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫
+                record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                  fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
+                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
+                  order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
+                    (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
+                  order {s} {z2} s<u1 with trio< s px | inspect supf1 s
+                  ... | tri< a ¬b ¬c | record { eq = eq1 } = ?
+                  ... | tri≈ ¬a b ¬c | record{ eq = eq1 } = ?
+                  ... | tri> ¬a ¬b c | record{ eq = eq1 } = ?
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
-                record { fcy<sup = ? ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫
-              ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } = ? where
-                 zc31 : supf0 u1 ≡ u1
-                 zc31 = ChainP.supu=u u1-is-sup
-                 zc32 : u1 o≤ x
-                 zc32 = OrdTrans u1≤x (OrdTrans z0≤1 z1≤x )
-                 zc30 : x ≡ u1
-                 zc30 with osuc-≡< zc32
-                 ... | case1 eq = sym (eq)
-                 ... | case2 u1<x = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op)) u1<x ⟫ )
+                record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
+                  fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
+                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
+              ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px)
+              ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
+              ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
               zc60 (fsuc w1 fc) with zc60 fc
               ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
               ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
@@ -748,8 +752,8 @@
                  ... | tri> ¬a ¬b c = {!!}
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px 
-                 ... | tri< a ¬b ¬c = UnionCF⊆ ? ? ( ZChain.csupf zc (o<→≤ a) )
-                 ... | tri≈ ¬a b ¬c = UnionCF⊆ ? ? ( ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
+                 ... | 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 px<b =  ⟪ {!!} , ch-is-sup b  o≤-refl {!!} {!!} ⟫  where
                      --   px< b ≤ x
                      -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1