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

changeset 816:648131d2b83c

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 Tue, 16 Aug 2022 22:36:14 +0900
parents d70f3f0681ea
children 26450ab6dd4e
files src/zorn.agda
diffstat 1 files changed, 7 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 16 21:54:03 2022 +0900
+++ b/src/zorn.agda	Tue Aug 16 22:36:14 2022 +0900
@@ -738,9 +738,9 @@
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
-                 UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o≤ x → z1 o≤ px → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 
-                 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x z1≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x z1≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
+                 UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o≤ x → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 
+                 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
                       zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w
                       zc60 {w} (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 ) 
@@ -803,21 +803,12 @@
                       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₁) ⟫ 
-                 chp10 : {u : Ordinal } → u o< x → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u
-                 chp10 = ?
-                 fc10 : {w : Ordinal } → u o< x → FClosure A f supf1 w → FClosure A f supf0 w 
-                 fc10 = ?
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl (ordtrans z<x <-osuc) (o<→≤ a)) ( ZChain.sup zc  a ) 
-                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = λ {w} lt → zc61 (subst (λ k → UnionCF A f mf ay supf1 k ∋ w) b lt) } where
-                     zc61 : {w : HOD} → UnionCF A f mf ay supf1 px ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc61 {w} ⟪ au , ch-init fc ⟫  with SUP.x<sup sup1 ⟪ au , ch-init fc ⟫ 
-                     ... | case1 eq = case1 eq
-                     ... | case2 lt = case2 lt
-                     zc61 {w} ⟪ au , ch-is-sup u u≤px is-sup fc ⟫ with SUP.x<sup sup1 ⟪ au , ch-is-sup u (subst (λ k → u o≤ k) (Oprev.oprev=x op) (ordtrans u≤px <-osuc))  ? ? ⟫ 
-                     ... | case1 eq = case1 eq
-                     ... | case2 lt = case2 lt
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl (ordtrans z<x <-osuc) ) ( ZChain.sup zc  a ) 
+                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
+                     zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
+                     zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) (o<→≤ z<x)  lt )
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b