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

diff -r f28f119bfa6f -r 3105feb3c4e1 src/zorn.agda
--- a/src/zorn.agda	Wed Oct 12 10:23:27 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 11:11:42 2022 +0900
@@ -1091,10 +1091,10 @@
                            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
+                             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 px<z1 | record { eq = eq1 }  with trio< sp1 px
@@ -1105,6 +1105,11 @@
                           --  supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1
                           asm : odef A (supf1 z1)
                           asm =  subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) 
+                          cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) 
+                          cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin
+                             supf0 px ≡⟨ sym (sf1=sf0 o≤-refl )  ⟩
+                             supf1 px ≡⟨ cong supf1 (sym sp1=px)  ⟩
+                             supf1 sp1 ∎  ))) where open ≡-Reasoning
                           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  ⟫ )