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

changeset 802:358c33d3a2bd

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, 09 Aug 2022 08:43:03 +0900
parents 8373b130ba41
children 7c6612b753b9
files src/zorn.agda
diffstat 1 files changed, 29 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Aug 08 14:35:12 2022 +0900
+++ b/src/zorn.agda	Tue Aug 09 08:43:03 2022 +0900
@@ -718,46 +718,19 @@
           no-extension : ¬  sp1 ≡ x → ZChain A f mf ay x
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
                ; initial = {!!} ; chain∋init = {!!}  ; sup=u = {!!} ; supf-is-sup = {!!} ; csupf = {!!} 
-              ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} }  where
-                 UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay supf0 x 
-                 UnionCF⊆ ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
-                 UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1 ; supu=u = su=u1 }  fc ⟫ with trio< u px
-                 ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = {!!} } fc ⟫  where
-                     order0 : {s z1 : Ordinal}  → s o< u → FClosure A f (supf0 s) z1 
-                        → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                     order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
-                     ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} {!!}  
-                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} {!!}  
-                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri> ¬a ¬b c | record {eq = eq1} = {!!}
-                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0  ; supu=u = {!!}} fc ⟫ where
-                     order0 : {s z1 : Ordinal}  → s o< u → FClosure A f (supf0 s) z1 
-                        → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                     order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
-                     ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} {!!}  
-                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} {!!}  
-                                                                          (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x {!!} )) where
-                         s≤u : s o≤ u
-                         s≤u = {!!}
-                         u=x : u ≡ x
-                         u=x with trio< u x
-                         ... | tri< a ¬b ¬c = {!!}
-                         ... | tri≈ ¬a b ¬c = b
-                         ... | tri> ¬a ¬b c = {!!}
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x su=u1 )) where
-                      u=x : u ≡ x
-                      u=x with trio< u x
-                      ... | tri< a ¬b ¬c = {!!}
-                      ... | tri≈ ¬a b ¬c = b
-                      ... | tri> ¬a ¬b c = {!!}
+              ;  chain⊆A = {!!} ;  f-next = ? ;  f-total = {!!} }  where
+                 UnionCF⊆ : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 x 
+                 UnionCF⊆ {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
+                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
+                      UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
                  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⊆ {!!} (ZChain.sup zc (o<→≤ a))
-                 ... | tri≈ ¬a b ¬c = SUP⊆ {!!} (ZChain.sup zc (o≤-refl0 b))
-                 ... | tri> ¬a ¬b c = SUP⊆ {!!} sup1
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
+                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
+                 ... | tri> ¬a ¬b c = SUP⊆ (λ lt  → chain-mono f mf ay _ ? (UnionCF⊆ ? lt )) sup1
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -844,18 +817,30 @@
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
           no-extension : ¬ spu ≡ x → ZChain A f mf ay x
-          no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = {!!} 
+          no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
                ; sup = sup ; supf-is-sup = sis
                ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
-                 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay (supfu a) x 
-                 UnionCF⊆ = {!!}
+                 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x 
+                 UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
+                 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
+                      UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+                 UnionCF0⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay psupf0 x 
+                 UnionCF0⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
+                 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
+                      UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = SUP⊆ {!!} (ZChain.sup (pzc z a) o≤-refl )
-                 ... | tri≈ ¬a b ¬c = SUP⊆ {!!} usup
-                 ... | tri> ¬a ¬b c = SUP⊆ {!!} usup
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) ?) ? )
+                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF0⊆ ?) usup
+                 ... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ ?) usup
                  sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z))
                  sis {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where