# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670121899 -32400
# Node ID d7ffe919d463f459c97ea79788c0763628e2e4bb
# Parent  fd26e0c4e648ad953713a71a180c2b6201a09c4e
...

diff -r fd26e0c4e648 -r d7ffe919d463 src/zorn.agda
--- a/src/zorn.agda	Sun Dec 04 10:30:24 2022 +0900
+++ b/src/zorn.agda	Sun Dec 04 11:44:59 2022 +0900
@@ -332,7 +332,7 @@
    field
       supf :  Ordinal → Ordinal
 
-      order : {x y w : Ordinal } → y o≤ z → x o< y → FClosure A f (supf x) w → w ≤ supf y
+      order : {x y w : Ordinal } → y o≤ z → x o< y → supf x o< z → FClosure A f (supf x) w → w ≤ supf y
 
       cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
 
@@ -397,13 +397,13 @@
      subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
          fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
          fc-total with trio< ua ub
-         ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) a₁ fca ) (s≤fc (supf ub) f mf fcb )
+         ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) a₁ ? fca ) (s≤fc (supf ub) f mf fcb )
          ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                   ct00 : * (& a) ≡ * (& b)
                   ct00 = cong (*) eq1
          ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
          fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
-         fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) c fcb ) (s≤fc (supf ua) f mf fca )
+         fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) c ? fcb ) (s≤fc (supf ua) f mf fca )
          ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                   ct00 : * (& a) ≡ * (& b)
                   ct00 = cong (*) (sym eq1)
@@ -454,7 +454,7 @@
    supf-idem {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
-       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b fc where
+       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b ? fc where
                su<b : u o< b
                su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
        z52 : supf (supf b) ≡ supf b
@@ -859,8 +859,8 @@
           m13 : supf0 px o< x → supf0 px o≤ sp1
           m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1)  m14 where
              m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
-             m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) (sfpx≤sp1 ?)
-             m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) (sfpx≤sp1 spx<x )
+             m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) (sfpx≤sp1 spx<x)
+             m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x ? fc) (sfpx≤sp1 spx<x )
 
           zc41 : ZChain A f mf< ay x
           zc41 =  record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
@@ -1033,7 +1033,14 @@
                         asp0 : odef A (supf0 u)
                         asp0 = ZChain.asupf zc
                     ... | tri≈ ¬a b ¬c = case2 ⟪ (init (subst (λ k → odef A k) b (ZChain.asupf zc) )
-                        (sym (trans (sf1=sf0 (zc-b<x _ u<x))  b ))) , ? ⟫
+                        (sym (trans (sf1=sf0 (zc-b<x _ u<x))  b ))) , spx<x ⟫ where
+                          spx<x : supf0 px o< x
+                          spx<x = osucprev ( begin
+                             osuc (supf0 px) ≡⟨ cong osuc (sym b) ⟩
+                             osuc (supf0 u) ≡⟨ cong osuc  (sym (sf1=sf0 (zc-b<x _ u<x) ))  ⟩
+                             osuc (supf1 u) ≡⟨ cong osuc  su=u ⟩
+                             osuc u ≤⟨ osucc u<x ⟩
+                             x ∎ ) where open o≤-Reasoning O
                     ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
 
                  is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
@@ -1043,13 +1050,13 @@
                     px<z = subst (λ k → px o< k) (sym z=x) px<x
                     zc22 : odef A (supf1 z)
                     zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z ))  ( MinSUP.as sup1 )
-                    z26 : supf1 px ≤ supf1 x
-                    z26 = subst₂ (λ j k → j ≤ k ) (sym (sf1=sf0 o≤-refl )) (sym (sf1=sp1 px<x )) (sfpx≤sp1 ?)
                     z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
                     z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz )
                     ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j  ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where
                         z25 : w ≤ supf0 px
                         z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz
+                        z26 : supf1 px ≤ supf1 x
+                        z26 = ?
                     ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) )
                     z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )
                         → supf1 z o≤ s
@@ -1058,9 +1065,9 @@
                         z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where
                             -- z=x , supf0 px o< x
                             z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x ≡ sp1 o≤ x ≡ z
-                            z28 = subst (λ k → supf0 px o< k) (sym z=x) ?
+                            z28 = subst (λ k → supf0 px o< k) (sym z=x) (proj2 fc)
                             z29 : supf0 px o≤ px
-                            z29 = zc-b<x _ ?
+                            z29 = zc-b<x _ (proj2 fc)
                             z27 : supf1 (supf0 px) ≡ supf0 px
                             z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 )
                             fc1 : FClosure A f (supf1 (supf0 px)) w
@@ -1097,12 +1104,12 @@
                                 u≤px = ordtrans u<x z≤px
 
                  order : {a b : Ordinal} {w : Ordinal} →
-                    b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b
-                 order {a} {b} {w} b≤x a<b fc with trio< b px
-                 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) ))
-                 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
+                    b o≤ x → a o< b → supf1 a o< x  → FClosure A f (supf1 a) w → w ≤ supf1 b
+                 order {a} {b} {w} b≤x a<b sa<x fc with trio< b px
+                 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b ? (fcup fc (o<→≤ (ordtrans a<b b<px) ))
+                 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b ? (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
                  ... | tri> ¬a ¬b px<b with trio< a px
-                 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) (sfpx≤sp1  ? ) --   supf1 a ≡ supf0 a
+                 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px ? fc) (sfpx≤sp1  ? ) --   supf1 a ≡ supf0 a
                  ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 ⟪ (subst (λ k → FClosure A f (supf0 k) w) a=px fc ) , ? ⟫ )
                  ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where  --   supf1 a ≡ sp1
                      zc22 : a o< osuc px
@@ -1172,14 +1179,14 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 with trio< (IChain.i ia)  (IChain.i ib)
                ... | tri< ia<ib ¬b ¬c with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
+                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib ? (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = cong (*) eq1
                ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
                uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
                uz01 | tri> ¬a ¬b ib<ia  with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
+                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia ? (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = sym (cong (*) eq1)