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

changeset 736:3c3e3a1291bb

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 Tue, 19 Jul 2022 15:14:50 +0900
parents 5dacaf73eba8
children 961abb22f2d9
files src/zorn.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 19 13:44:33 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 15:14:50 2022 +0900
@@ -475,8 +475,8 @@
                  px<x : px o< x
                  px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-                 m01 with trio< b px 
-                 ... | tri> ¬a ¬b c = ⊥-eim ()
+                 m01 with trio< b px    --- px  < b < x
+                 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
                  ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
                     m03 = ?