# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665537807 -32400
# Node ID f28f119bfa6f7642454fdf1a7275bde701a1d8cf
# Parent  fec6064b44befbb846bf6c14cedf6b52196e4c50
...

diff -r fec6064b44be -r f28f119bfa6f src/zorn.agda
--- a/src/zorn.agda	Wed Oct 12 01:46:29 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 10:23:27 2022 +0900
@@ -1079,32 +1079,35 @@
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
                      cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px)
                      cs01 spx<px = ZChain.csupf zc spx<px
-                     cs00 : supf1 (supf1 px) ≡ supf1 px
-                     cs00 = ?
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                      csupf2 with  trio< z1 px | inspect supf1 z1
                      csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
-                     ... | case1 eq =  ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
-                             record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
-                          -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
-                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
-                          supu=u = ? -- ZChain.sup=u zc ? ? ?
                      ... | case2 lt  = zc12 (case1 cs03)  where
                            cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
                            cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
+                     ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
+                     ... | case1 sfz=sfpx =  zc12 (case2 (init (ZChain.asupf zc) cs04 )) where
+                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
+                           supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx)
+                           cs04 : supf0 px ≡ supf0 z1 
+                           cs04 = begin
+                            supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
+                            supf1 px ≡⟨ sym sfz=sfpx ⟩
+                            supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a)  ⟩
+                            supf0 z1 ∎ where open ≡-Reasoning
+                     ... | case2 sfz<sfpx =  ? ---   supf0 z1 o< supf0 px
                      csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
-                     csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
+                     csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 }  with trio< sp1 px
+                     ... | tri< sp1<px ¬b ¬c = ? --  sp1 o< px, supf0 sp1 ≡  supf0 px, sp1 o< z1
+                     ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
-                          --  supf1 z1 ≡ sp1, px o< z1, sp1 o< x
+                          --  supf1 z1 ≡ sp1, px o< z1, sp1 o< x  -- sp1 o< z1
+                          --  supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1
                           asm : odef A (supf1 z1)
-                          asm =  subst (λ k → odef A k ) (sym (sf1=sp1 c)) ( MinSUP.asm sup1) 
-                          sp1=px : sp1 ≡ px
-                          sp1=px with trio< sp1 px
-                          ... | tri< a ¬b ¬c = ? --  sp1 o< px, supf0 sp1 ≡  supf0 px
-                          ... | tri≈ ¬a b ¬c = b 
-                          ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
+                          asm =  subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) 
                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
                           supu=u = ?
+                     ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)