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

diff -r 0dd8cc755ec9 -r e5cde0cd6a83 src/zorn.agda
--- a/src/zorn.agda	Sat Jul 16 04:11:07 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 08:19:50 2022 +0900
@@ -652,6 +652,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
                    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
@@ -745,8 +747,14 @@
                             * 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 = ⟪ proj1 z30 , ? ⟫ where
-                    z30 = ZChain.is-max (uzc za) ? ? ab (case2 ?) a<b 
+                ... | 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 = ?
 
                 --⊥-elim ( ¬x=sup record { 
                 --      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) ?