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

changeset 720:6c9fed204440

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 Sat, 16 Jul 2022 00:45:38 +0900
parents b0cad3ec7da0
children 562ddd33fe21
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 15 21:39:32 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 00:45:38 2022 +0900
@@ -628,10 +628,6 @@
                       ... | tri≈ ¬a b ¬c = ? where
                           zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr)
                           zc13 = HasPrev.ay pr 
-                          zc12 : ?
-                          zc12 with proj1 (mf _ (A∋fcs _ f mf fc ) ) | zc13  -- u is sup and has prev
-                          ... | case1 x | ⟪ apz , ach ⟫ = ?
-                          ... | case2 x | ⟪ apz , ach ⟫ = ?
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
                 ... | tri≈ ¬a b=px ¬c = zc15 where
                        zc14 : f (HasPrev.y pr) ≡ b
@@ -666,7 +662,9 @@
                             HasPrev A pchain ab f ∨ IsSup A pchain   ab →
                             * a < * b → odef pchain b
                 z18 {a} {b} za b<x ab P a<b with trio< b px
-                ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b 
+                ... | tri< lt ¬b ¬c = ? where
+                    z20 : odef pchain b
+                    z20 = chain-mono ( ZChain.is-max zc ? lt ab ? a<b )
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
                 ... | tri≈ ¬a b=px ¬c with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )