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

changeset 998:e5f46d08c074

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 Thu, 17 Nov 2022 19:04:06 +0900
parents 908369b2d08b
children 3ffbdd53d1ea
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Nov 17 17:04:47 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 19:04:06 2022 +0900
@@ -1072,10 +1072,12 @@
                       ... | 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
+                      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
                       cp1 = record { fcy<sup = λ {z} fc → ? 
                                ; order =  λ {s} {z} s<u fc  → ? 
-                               ; supu=u = ? }
+                               ; supu=u = spx=px }
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
 
                  zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z