# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657669392 -32400
# Node ID e59bcd41462df3240b7da2222b5d31c55dbd6c89
# Parent  799963f352d64977cd59275bbf080e697d1c578c
initial chain has no maximality

diff -r 799963f352d6 -r e59bcd41462d src/zorn.agda
--- 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