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

changeset 515:5faeae7cfe22

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε-induction does not work on Zorn
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 16 Apr 2022 12:10:09 +0900
parents 97c8abf28706
children 286016848403
files src/zorn.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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) )