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

changeset 914:0d8d230e4b2b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
this csupf is bad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 Oct 2022 19:51:00 +0900
parents d5293a7c2ec4
children
files src/zorn.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Oct 12 14:45:53 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 19:51:00 2022 +0900
@@ -1120,12 +1120,14 @@
                  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 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 sw<z (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) lt )
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c =  ?
+                 ... | case2 lt = ? where
+                     csupfpx : supf0 w o< z → odef (UnionCF A f mf ay supf0 z) (supf0 w) 
+                     csupfpx sw<z = ZChain.csupf zc sw<z (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) lt )
+                     cs10 : odef (UnionCF A f mf ay supf1 z) (supf1 w) 
+                     cs10 with trio< w px
+                     ... | tri< sw<z ¬b ¬c = ? 
+                     ... | 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)