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

changeset 706:e59bcd41462d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial chain has no maximality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 13 Jul 2022 08:43:12 +0900
parents 799963f352d6
children e9ddbf84d699
files src/zorn.agda
diffstat 1 files changed, 4 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Jul 13 07:55:13 2022 +0900
+++ b/src/zorn.agda	Wed Jul 13 08:43:12 2022 +0900
@@ -498,6 +498,10 @@
             * a < * b → odef (UnionCF A f mf ay isupf x) b
           imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf x) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
           imax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
+          -- with IsSup.x<sup sup (inext 
+          -- ... | case1 a=b = ?
+          -- ... | case2 a<b = ?
+          -- ⊥-elim ( <-irr (case2 ? ) ( IsSup  ) )
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x