# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657960243 -32400
# Node ID 97efa6b434c9c2094e4922010bde919d170c35e2
# Parent  e5cde0cd6a838afbf0ebef8355d6521363661957
...

diff -r e5cde0cd6a83 -r 97efa6b434c9 src/zorn.agda
--- a/src/zorn.agda	Sat Jul 16 08:19:50 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 17:30:43 2022 +0900
@@ -241,6 +241,12 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
+record IsSup>b (A : HOD) (b : Ordinal) (p : Ordinal) : Set n where
+  field
+     x2 : Ordinal
+     ax2 : odef A x2
+     b<x2 : b o< x2
+     is-sup>b : IsSup A (* p) ax2
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
@@ -304,6 +310,12 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
+-- IsSup→Maximal : {A B : HOD} → {s : Ordinal } → ( B⊆A : B ⊆' A ) → ( bs : odef B s )→ IsSup A B (B⊆A bs) → Maximal A
+-- IsSup→Maximal {A} {B} {s}  B⊆A bs is-sup 
+--       = record { maximal = * s ; A∋maximal = subst (λ k → odef A k ) (sym &iso) (B⊆A bs) ;  ¬maximal<x = is00 } where
+--    is00 : {z : HOD} → A ∋ z → ¬ (* s < z)
+--    is00 = ?
+
 -- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
 --
 -- data Chain is total
@@ -346,8 +358,8 @@
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
-     ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
+ChainP-next A f mf {y} ay supf {x} {z} cp = ? --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
+     -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -652,8 +664,8 @@
                        x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) 
                           (IsSup.x<sup b=sup (chain-mono zy) )  } ) 
                 ... | tri< b<px ¬b ¬c = chain-mono (ZChain.is-max zc pa b<px ab (case2 record { x<sup = sup1 }) a<b) where
-                   -- b=sup contradicts u = px
-                   --    FClosure px is in pchain, if sup (fc px) o< x , it is the Maximal
+                   -- if b=sup and ¬ Isup>b , then b is Maximal
+                   --   px o< sup (fc u) ∈ pchain contradicts b=sup ( x o< sup x )
                    z19 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px
                    z19 {z} za@record {proj1 =  az ; proj2 =  record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } } 
                          with trio< (UChain.u (proj2 za))  px
@@ -747,14 +759,11 @@
                             * a < * b → odef pchain b
                 z18 {a} {b} za b<x ab P a<b with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
-                ... | case2 b=sup = ⟪ ab , record { u = UChain.u (proj2 za) ; u<x = ? ; uchain = ? }  ⟫ where
-                    --   FClosure b o< x and A ∋ sup (fc b)  → pchain ∋ sup (fc b) >> b conradicts b=sup
-                    z30 : odef (UnionCF A f mf ay (ZChain.supf (uzc za) ) (UChain.u (proj2 za)) ) b
-                    z30 with UChain.u<x (proj2 za)
-                    ... | case1 u<x = ⟪ ab , record { u = (UChain.u (proj2 z31)) ; u<x =  case1 ? ; uchain = ? }   ⟫ where
-                      z31 = ZChain.is-max (uzc za) ⟪ proj1 za , 
-                         record { u = (UChain.u (proj2 za)) ; u<x =  case1 ? ; uchain = ? }   ⟫ ?  ab (case2 ?) a<b 
-                    ... | case2 u=0 = ?
+                ... | case2 b=sup = ⟪ ab , record { u = UChain.u (proj2 z30) ; u<x = ? ; uchain = ? } ⟫ where
+                    ob<x : osuc b o< x
+                    ob<x = ?
+                    z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b
+                    z30 = ZChain.is-max (pzc _ ob<x) ? <-osuc  ab (case1 ?) a<b 
 
                 --⊥-elim ( ¬x=sup record { 
                 --      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) ?