# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650078609 -32400
# Node ID 5faeae7cfe22eca6c6bf063d9a47aa125fa641ce
# Parent  97c8abf287062d6423175d97b1e32b9a3228705a
 ε-induction does not work on Zorn

diff -r 97c8abf28706 -r 5faeae7cfe22 src/zorn.agda
--- a/src/zorn.agda	Sat Apr 16 11:51:43 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 12:10:09 2022 +0900
@@ -392,9 +392,15 @@
      ... | tri> ¬a ¬b c with ODC.∋-p O A (* x)
      ... | no ¬Ax = {!!} where
      ... | yes ax = {!!}
-     ... | no not = {!!} where
      zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
      zorn03 x = TransFinite ind  x
+     zorn07 : (x : HOD) → (ax : A ∋ x ) → OSup> A (d→∋ A ax) ∨ Maximal A ∨ InFiniteIChain A (d→∋ A ax)
+     zorn07 x = ε-induction (λ {x} prev ax →  Zorn-lemma-3case 0<A PO (me {A} {x}  ax ) ) x
+     zorn05 : Maximal A 
+     zorn05 with zorn07 A {!!}
+     ... | case1 chain = {!!}
+     ... | case2 (case1 m) = m
+     ... | case2 (case2 chain) = {!!}
      zorn04 : Maximal A 
      zorn04 with zorn03 (& A)
      ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.max chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )