# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649740620 -32400
# Node ID a97a1f1e27fa039f9b0282d5d81329f58446af38
# Parent  5b1cfaf4c4ffe24703892d6dd9857abf3e16ecc5
...

diff -r 5b1cfaf4c4ff -r a97a1f1e27fa src/zorn.agda
--- 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)