# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667784233 -32400
# Node ID 4fdf889ca95a5909096170155b364c490aaeecbe
# Parent  980bc43ca6c111adbccf529d9468539018d4e5d8
...

diff -r 980bc43ca6c1 -r 4fdf889ca95a src/zorn.agda
--- a/src/zorn.agda	Mon Nov 07 08:04:35 2022 +0900
+++ b/src/zorn.agda	Mon Nov 07 10:23:53 2022 +0900
@@ -883,7 +883,10 @@
           --  x < supf px  → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
 
           zc43 :  ( x o< sp1 ) ∨ ( sp1 o≤ x )
-          zc43 = ?
+          zc43 with trio< x sp1
+          ... | tri< a ¬b ¬c = case1 a
+          ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
+          ... | tri> ¬a ¬b c = case2 (o<→≤ c)
           
           zc41 : ZChain A f mf ay x
           zc41 with zc43
@@ -1043,6 +1046,14 @@
                            (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z)))  (o≤-refl0 b)
                      ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 ))
 
+                 3cases : (¬ (supf0 px ≡ px)) ∨ ( ¬ (supf0 px o< sp1 )) ∨ ( (supf0 px ≡ px) ∧  (supf0 px o< sp1 )) 
+                 3cases with o≡? (supf0 px) px
+                 ... | no ne = case1 ne
+                 ... | yes eq with trio< (supf0 px) sp1
+                 ... | tri< a ¬b ¬c = case2 (case2 ⟪ eq , a ⟫ )
+                 ... | tri≈ ¬a b ¬c = case2 (case1 ¬a )
+                 ... | tri> ¬a ¬b c = case2 (case1 ¬a )
+
                  zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
                  zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
                  zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
@@ -1164,18 +1175,15 @@
                      --  z1 ≡ px , supf0 px ≡  px
                      psz1≤px :  supf1 z1 o≤ px
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
-                     sf0px<sp1 : supf0 px o< sp1  -- px o< sp1 o≤ x .. sp1 ≡ x
-                     sf0px<sp1 = ?
                      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
-                     ... | case2 lt  = zc12 ? ? (case1 cs03)  where
+                     csupf2 with 3cases
+                     ... | case2 (case2 p) with  trio< z1 px | inspect supf1 z1
+                     ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
+                     ... | case2 lt  = zc12 (proj1 p) (proj2 p) (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)
+                     ... | case1 sfz=sfpx =  zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where
                            cs04 : supf0 px ≡ supf0 z1
                            cs04 = begin
                              supf0 px ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩
@@ -1187,10 +1195,17 @@
                            cs05 : px o< supf0 px
                            cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
                            cs06 : supf0 px o< osuc px
-                           cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ?
-                     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 } = ?
-                     -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
+                           cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x
+                     csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (proj1 p) (proj2 p) 
+                           (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
+                     csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } =  ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where
+                           cs08 : px o< sp1
+                           cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p )
+                           cs09 : sp1 o< osuc px
+                           cs09  = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
+
+                     csupf2 | case2 (case1 p) = ?
+                     csupf2 | case1 p = ?
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?