# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668783875 -32400
# Node ID ac182ad5bfd2185a55a0dc933285c5921e492d29
# Parent  2808471040c06bb47f7190fb6cd4d75cf3b88790
...

diff -r 2808471040c0 -r ac182ad5bfd2 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 18 23:54:13 2022 +0900
+++ b/src/zorn.agda	Sat Nov 19 00:04:35 2022 +0900
@@ -511,8 +511,8 @@
        fsp≤sp : f sp <=  sp
        fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
 
-   csupf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o< z  → supf (supf b) ≡ supf b
-   csupf-idem  mf< {b} b≤z sfb<x = z52 where
+   supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
+   supf-idem  mf< {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
        z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) 
@@ -523,7 +523,7 @@
                su<z : supf u o< z
                su<z = subst (λ k → k o< z ) (sym (ChainP.supu=u is-sup)) ( ordtrans<-≤ u<b b≤z )
        z52 : supf (supf b) ≡ supf b
-       z52 = sup=u asupf (o<→≤ sfb<x) ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
+       z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
 UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
@@ -1066,19 +1066,8 @@
                           spx = supf0 px
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
-                          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))) ⟫ )
+                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl ? )
                           fc1 : FClosure A f (supf1 spx) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
                           order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)