# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661820565 -32400
# Node ID 962a9f3dbd3c6c9e224b2790b322415989170101
# Parent  01361e10ad96a9afd7b4f2c83ec9e49c3f41279f
...

diff -r 01361e10ad96 -r 962a9f3dbd3c src/zorn.agda
--- a/src/zorn.agda	Mon Aug 29 19:56:39 2022 +0900
+++ b/src/zorn.agda	Tue Aug 30 09:49:25 2022 +0900
@@ -271,6 +271,15 @@
 UnionCF A f mf ay supf x
    = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
+supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )   
+   → supf x o< supf y → x o<  y 
+supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
+... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) )
+... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
+... | case2 lt = ⊥-elim ( o<> sx<sy lt )
+
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -764,9 +773,11 @@
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
 
           no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = ?
+          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = supf-mono
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
+                 supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
+                 supf-mono = ?
                  pchain0=1 : pchain ≡ pchain1
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
@@ -777,26 +788,31 @@
                           ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                           ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
                           zc12 (init asp refl ) with trio< u1 px | inspect supf1 u1
-                          ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x ? ) 
+                          ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x (o<→≤ px<x) ) 
                             record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
                               fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
                               fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
                               order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
                                 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-                              order {s} {z2} s<u1 fc with trio< s px 
-                              ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
-                              ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
-                              ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? ))  --  px o< s < u1 < px
-                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x ? ) 
+                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
+                              ... | tri< a ¬b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
+                              ... | tri≈ ¬a b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
+                              ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans zc14 a) )) where  --  px o< s < u1 < px
+                                 zc14 :  s o< u1
+                                 zc14 = supf-inject0 supf-mono (subst₂ (λ j k → j o< k ) (sym eq2) refl s<u1 )
+                              ---   s ≡ sp1, px<s = px o< sp1
+                          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x (o<→≤ px<x) ) 
                             record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
                               fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
                               fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
                               order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 →
                                 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
-                              order {s} {z2} s<u1 fc with trio< s px 
-                              ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
-                              ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc )
-                              ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b ? ) ))  --  px o< s < u1 = px
+                              order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
+                              ... | tri< a ¬b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
+                              ... | tri≈ ¬a b ¬c | _ = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup (subst₂ (λ j k → j  o< k) refl eq1 s<u1) fc )
+                              ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b zc14 ) ))  where --  px o< s < u1 = px 
+                                 zc14 :  s o< u1
+                                 zc14 = supf-inject0 supf-mono (subst₂ (λ j k → j o< k ) (sym eq2) refl s<u1 )
                           ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x 
                           ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
                           ... | case2 lt = ⊥-elim ( o<> lt px<u1 )