# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665393904 -32400
# Node ID 02f250be89e25b0fd35f819becc2c558d5810ecf
# Parent  e6a282eb12feb4e008966b7b7f45d7c8c9af5037
...

diff -r e6a282eb12fe -r 02f250be89e2 src/zorn.agda
--- a/src/zorn.agda	Mon Oct 10 12:20:38 2022 +0900
+++ b/src/zorn.agda	Mon Oct 10 18:25:04 2022 +0900
@@ -1057,21 +1057,26 @@
                          ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } 
 
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
-                 csupf1 {z1} sz1<x with trio< (supf1 z1) px
-                 ... | tri< a ¬b ¬c = csupf0 where
-                     zc18 : supf1 z1 ≡ supf0 z1
-                     zc18 = sf1=sf0 ?
-                     csupf0 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
-                     csupf0 with ZChain.csupf zc (subst (λ k → k o< px) zc18 a )
-                     ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , ch-init ? ⟫
-                     ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , 
-                          ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ?  ?  ⟫ 
-                 ... | tri≈ ¬a b ¬c = ⟪ asm , ch-is-sup (supf1 z1) sz1<x ? (init asm1 ? ) ⟫ where
-                     asm : odef A (supf1 z1)
-                     asm =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
-                     asm1 : odef A (supf1 (supf1 z1))
-                     asm1 =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫  ) 
+                 csupf1 {z1} sz1<x = csupf2 where
+                     --  z1 o< px → supf1 z1 ≡ supf0 z1
+                     --  z1 ≡ px , supf0 px o< px   .. px o< z1, x o≤ z1 ...  supf1 z1 ≡ sp1
+                     --  z1 ≡ px , supf0 px ≡  px
+                     psz1≤px :  supf1 z1 o≤ px
+                     psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
+                     csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
+                     csupf2 with  trio< z1 px
+                     csupf2 | tri< a ¬b ¬c  with osuc-≡< psz1≤px
+                     ... | case1 eq = ? -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
+                     ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
+                     ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) ? ab , ch-init ? ⟫
+                     ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? , 
+                               ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ?  ?  ⟫ 
+                     csupf2 | tri≈ ¬a b ¬c = ? where  -- supf1 z1 ≡ supf0 z1, z1 ≡ px
+                          asm : odef A (supf1 z1)
+                          asm =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
+                          asm1 : odef A (supf1 (supf1 z1))
+                          asm1 =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
+                     csupf2 | tri> ¬a ¬b c = ?
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)