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

changeset 913:d5293a7c2ec4

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 Wed, 12 Oct 2022 14:45:53 +0900
parents 870a6b57dd39
children 0d8d230e4b2b
files src/zorn.agda
diffstat 1 files changed, 6 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Oct 12 14:03:38 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 14:45:53 2022 +0900
@@ -1119,10 +1119,13 @@
 
                  csupfp : {w z : Ordinal } → supf1 w o< z → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 w) 
                  csupfp {w} {z} sw1<z z≤x with osuc-≡< z≤x
-                 ... | case1 eq = ?
-                 ... | case2 lt = ?  where
+                 ... | case1 refl = csupf1 sw1<z
+                 ... | case2 lt with trio< (supf0 w) z
+                 ... | tri< sw<z ¬b ¬c = ? where
                      csupfpx : odef (UnionCF A f mf ay supf0 z) (supf0 w) 
-                     csupfpx = ZChain.csupf zc ? ?
+                     csupfpx = ZChain.csupf zc sw<z (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) lt )
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b c =  ?
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)