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

changeset 936:f160556a7c9a

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 Mon, 24 Oct 2022 16:16:15 +0900
parents ed711d7be191
children 3a511519bd10
files src/zorn.agda
diffstat 1 files changed, 4 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 24 16:06:18 2022 +0900
+++ b/src/zorn.agda	Mon Oct 24 16:16:15 2022 +0900
@@ -1366,9 +1366,7 @@
            z22 : sp o< & A
            z22 = z09 asp
            x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
-           x<sup bz with SUP.x<sup sp1 bz 
-           ... | case1 eq = case1 ?
-           ... | case2 lt = case2 ?
+           x<sup bz = SUP.x<sup sp1 bz 
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
@@ -1397,12 +1395,12 @@
                ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  * sp )
-               z15  = ? -- x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  SUP.sup sp1 )
+               z15  = x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
-               ... | case2 lt = ¬a ?
+               ... | case2 lt = ¬a lt
 
 
      -- ZChain contradicts ¬ Maximal