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

changeset 465:aba3d15ad45c

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, 22 Mar 2022 12:10:15 +0900
parents 5acf6483a9e3
children 14b0e0aa6487
files src/ODC.agda
diffstat 1 files changed, 4 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODC.agda	Tue Mar 22 07:31:46 2022 +0900
+++ b/src/ODC.agda	Tue Mar 22 12:10:15 2022 +0900
@@ -121,18 +121,10 @@
 
 record ZChain ( A : HOD ) (x : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
-      a : HOD
-      a<A :  A ∋ a 
-      x<a :  {y : HOD} → A ∋ y → & y o< & a →  y < a
-
-record ZPrev ( A : HOD ) (x : Ordinal)  : Set (suc n) where
-   field
-      prev : Ordinal
-      A∋p : odef A prev
-      p<x : prev o< x
-
-find-prev : ( A : HOD ) (x : Ordinal) → o∅ o< x → ZPrev A x
-find-prev = {!!}
+      NOMAX : OD
+      Chain : OD
+      nomax : (y m : Ordinal) → def NOMAX y → y o< x → ¬ ( * y < * m )
+      chain : (y : Ordinal) → def Chain y → NOMAX == od od∅  → SUP A (* y) _<_
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A