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

changeset 823:497b5db603e7

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, 18 Aug 2022 12:22:45 +0900
parents c97cc257374b
children 8a06fe74721b
files src/zorn.agda
diffstat 1 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Aug 18 11:48:29 2022 +0900
+++ b/src/zorn.agda	Thu Aug 18 12:22:45 2022 +0900
@@ -799,7 +799,10 @@
                  ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } =  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
                  sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))
-                 sis {z} z≤x = {!!}
+                 sis {z} z<x with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x  ⟫ )
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip