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

diff -r 19ae0591c6dd -r b9dfe9bc8412 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 18 17:58:48 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 18:14:41 2022 +0900
@@ -1080,48 +1080,32 @@
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
-                      fc1 : FClosure A f (supf1 px) w
-                      fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym (sf1=sf0 o≤-refl )) ) fc
                       csupf1 : odef (UnionCF A f mf ay supf1 b) w
                       csupf1 with trio< (supf0 px) x
-                      ... | tri< sfpx<x ¬b ¬c = csupf2 where
-                          -- supf0 px o< x ,   supf0 px is member of (UnionCF A f mf ay supf1 x)
-                          csupf2 : odef (UnionCF A f mf ay supf1 b) w
-                          csupf2 with osuc-≡< ((zc-b<x _ sfpx<x) )
-                          ... | case1 spx=px = ⟪ z53 , ch-is-sup px (subst (λ k → px o< k ) (sym b=x) px<x) cp1 fc1 ⟫  where 
-                              -- supf0 px ≡ px
-                              order : {s z1 : Ordinal} → supf1 s o< supf1 px → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
-                              order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
-                                   (trans (sym (ZChain.supf-is-minsup zc o≤-refl)) (sym (sf1=sf0 o≤-refl)) )
-                                   (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                       o≤-refl (fcup fcs (o<→≤ (supf-inject0 supf1-mono ss<spx)) ) ))
-                              cp1 : ChainP A f mf ay supf1 px
-                              cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 o≤-refl)) 
-                                  ( 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 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 )) 
+                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx ? cp1 fc1 ⟫  where
+                          spx = supf0 px
+                          fc1 : FClosure A f (supf1 spx) w
+                          fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) ? ) fc
+                          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) 
+                          -- 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 )) 
+                          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 ? )) 
+                          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 = ? }