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

changeset 500:a97a1f1e27fa

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, 12 Apr 2022 14:17:00 +0900
parents 5b1cfaf4c4ff
children 5a166a832472
files src/zorn.agda
diffstat 1 files changed, 6 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Apr 12 14:10:44 2022 +0900
+++ b/src/zorn.agda	Tue Apr 12 14:17:00 2022 +0900
@@ -151,7 +151,12 @@
         zc3 : {y : Element A} → IChainSet x ∋ elm y → ¬ (& (elm x) o< & (elm y))
         zc3 = {!!}
         zcind : (z : Ordinal ) → ((y : Ordinal) → y o< z → Dec (InFiniteIChain x y ) ) → Dec (InFiniteIChain x z)
-        zcind z prev = {!!}
+        zcind z prev with trio< (& A) z
+        ... | tri< a ¬b ¬c = {!!}
+        ... | tri≈ ¬a b ¬c = {!!}
+        ... | tri> ¬a ¬b c with ODC.∋-p O A (* z)
+        ... | no nota = {!!}
+        ... | yes az = {!!}
         zc4 : Dec (InFiniteIChain x (& A))
         zc4 = TransFinite zcind (& A)