# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667959811 -32400
# Node ID 49cf50d451e1abf006df9d9f4c4656700a083efc
# Parent  6229017a61767a11d8b7269fe453a4e6cf512fda
...

diff -r 6229017a6176 -r 49cf50d451e1 src/zorn.agda
--- a/src/zorn.agda	Wed Nov 09 05:00:56 2022 +0900
+++ b/src/zorn.agda	Wed Nov 09 11:10:11 2022 +0900
@@ -1178,60 +1178,45 @@
                        UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ 
                          (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) 
                          (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
-                 -- px o< z1 , px o≤ supf1 z1  -->   px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1
-                 --      supf1 px ≡ sp1 o< supf1 x
+                 -- px o< z1 , supf1 z1 o< x  ->   sp1 o≤ z1   -- sp1 o≤ supf1 x
+                 -- px o≤ supf1 z1 ,  supf1 z1 o< x -> supf1 z1 ≡ px --> z1 o≤ px → supf0 z1 ≡ px
+                                                                     --> px o< x1 → sp1 ≡ px
 
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
                  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 opx=x) sz1<x
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                     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 (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)  ⟩
-                             supf1 px ≡⟨ sym sfz=sfpx ⟩
-                             supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a)  ⟩
-                             supf0 z1 ∎ where open ≡-Reasoning
-                     ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫  )  where
-                            --- supf1 z1 ≡ px , z1 o< px ,  px ≡ supf0 z1 o< supf0 px o< x
-                           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₂ (λ 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) with trio< (supf0 px) sp1 --  ¬ (supf0 px o< sp1  --  sp1 o≤ supf px)
-                     ... | tri< a ¬b ¬c = ⊥-elim (p a)
-                     ... | tri≈ ¬a b ¬c = ?
-                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c )
-                     csupf2 | case1 p with trio< (supf0 px) px           --  ¬ (supf0 px ≡ px )
-                     ... | tri< sf0px<px ¬b ¬c = ? where
-                           cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px)
-                           cs10 = ZChain.csupf zc sf0px<px
-                     ... | tri≈ ¬a b ¬c = ⊥-elim (p b)
-                     ... | tri> ¬a ¬b px<sf0px = ? where
-                           cs11 : px o< z1 →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                           cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) 
-                              (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 )))  sfpx≤sp1 ) sz1<x) ⟫ )
-                           cs12 : z1 o≤ px →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                           cs12 = ?
-
+                     csupf2 with osuc-≡< psz1≤px 
+                     ... | case2 lt with trio< z1 px | inspect supf1 z1
+                     ... | tri< a ¬b ¬c  | record { eq = eq } = 
+                         subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o<→≤ a ))
+                     ... | tri≈ ¬a b ¬c  | record { eq = eq } = 
+                         subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o≤-refl0 b ))
+                     ... | tri> ¬a ¬b px<z1 | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup sp1 cs00 ? (init asupf1 ssp1=sp1 ) ⟫ where
+                         ssp1=sp1 : supf1 sp1 ≡ sp1
+                         ssp1=sp1 = ?
+                         cs00 : supf1 sp1 o≤ supf1 x
+                         cs00 = ?
+                     csupf2 | case1 psz1=px with trio< z1 px | inspect supf1 z1
+                     ... | tri< a ¬b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where
+                         --  spuf1 z1 == px o< x , z1 o< px, 
+                         cs03 : supf0 z1 o< px
+                         cs03 = ?
+                         cs02  : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
+                         cs02 = ZChain.csupf zc cs03
+                         cs01 : supf1 px ≡ supf0 z1
+                         cs01 = ?
+                         cs00 : supf1 px o≤ supf1 x
+                         cs00 = supf1-mono (o<→≤ px<x)
+                     ... | tri≈ ¬a b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where
+                         cs01 : supf1 px ≡ supf0 z1
+                         cs01 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b) )
+                         cs00 : supf1 px o≤ supf1 x
+                         cs00 = supf1-mono (o<→≤ px<x)
+                     ... | tri> ¬a ¬b c | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup x o≤-refl ? (init asupf1 cs01 ) ⟫ where
+                         cs01 : supf1 x ≡ sp1
+                         cs01 = sf1=sp1 px<x
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where