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

changeset 1037:23e185ef2737

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 Fri, 02 Dec 2022 19:14:41 +0900
parents 23a8e4d558e0
children dfbac4b59bae
files src/zorn.agda
diffstat 1 files changed, 6 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 02 15:49:50 2022 +0900
+++ b/src/zorn.agda	Fri Dec 02 19:14:41 2022 +0900
@@ -1057,9 +1057,13 @@
                         → supf1 z o≤ s
                     z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where
                         z25 : {w : Ordinal } → odef pchainpx w → w ≤ s 
-                        z25 {w} (case2 fc) = sup ⟪ ? , ch-is-sup px px<z z27 (fcpu fc ?) ⟫ where
+                        z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) ? ?  ? ⟫ where
                             z27 : supf1 px ≡ px    --- sp1 o≤ x
-                            z27 = ?
+                            z27 = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc ? ? ? )
+                            z29 : supf0 px o≤ z
+                            z29 = ? --    supf0 px ≡ supf1 px o≤ supf1 x o≤ x ≡ z
+                            z28 : supf0 px o< z
+                            z28 = ?
                         z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
                         z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc  ⟫) = sup ⟪ ua , ch-is-sup u u<z
                              (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where