# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668761928 -32400
# Node ID 19ae0591c6dd074d6dc0539e2c7b561ee213eced
# Parent  e18d9764365acff2488256345aec802236cdcc04
...

diff -r e18d9764365a -r 19ae0591c6dd src/zorn.agda
--- a/src/zorn.agda	Fri Nov 18 17:15:47 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 17:58:48 2022 +0900
@@ -1100,7 +1100,31 @@
                                   ( ZChain.fcy<sup zc o≤-refl fc )
                                        ; order =  order
                                        ; supu=u = trans (sf1=sf0 o≤-refl)  spx=px } 
-                          ... | case2 spx<px = ⟪ z53 , ch-is-sup ? ? ? ? ⟫  
+                          ... | case2 spx<px = ⟪ z53 , ch-is-sup spx ? ? ? ⟫  where
+                              spx = supf0 px
+                              z54 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
+                              z54 {z} ⟪ az , ch-init fc ⟫ = ZChain.fcy<sup zc o≤-refl fc
+                              z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = subst (λ k → (z ≡ k) ∨ (z << k )) 
+                                       (sym (ZChain.supf-is-minsup zc o≤-refl)) 
+                                       (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< u<px o≤-refl fc )) where
+                                   u<px : u o< px
+                                   u<px = ZChain.supf-inject zc ( subst (λ k → k o< supf0 px) (sym (ChainP.supu=u is-sup)) u<b )
+                              -- u<b    : u o< supf0 px
+                              -- is-sup : ChainP A f mf ay (ZChain.supf zc) u
+                              -- fc     : FClosure A f (ZChain.supf zc u) z
+                              z52 : supf1 (supf0 px) ≡ supf0 px
+                              z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x) 
+                                     ⟪ record { x≤sup = z54  } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ )
+                              order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
+                              order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
+                                   (trans (sym (ZChain.supf-is-minsup zc ? )) (sym ? ) )
+                                   (MinSUP.x≤sup (ZChain.minsup zc ?) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
+                                       ? (fcup fcs ? ) ))
+                              cp1 : ChainP A f mf ay supf1 spx
+                              cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 ? )) 
+                                  ( ZChain.fcy<sup zc ? fc )
+                                       ; order =  order
+                                       ; supu=u = ? }
                       ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
                           -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
                           m12 : supf0 px ≡ sp1