# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658656884 -32400
# Node ID 944f50265914b8623fe255f4d7429aa0d0f91e62
# Parent  a2947dfff80dbc9f86142f26fae7dcfb01b84470
...

diff -r a2947dfff80d -r 944f50265914 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 24 16:40:35 2022 +0900
+++ b/src/zorn.agda	Sun Jul 24 19:01:24 2022 +0900
@@ -451,8 +451,8 @@
            px = Oprev.oprev op
            zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
            zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
-           fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
-           fcy<sup {u} {w} u≤x fc = ?
+           -- fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
+           -- fcy<sup {u} {w} u≤x fc = ?
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
@@ -477,7 +477,7 @@
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ? -- b = px case,  u = px  u< osuc x 
+                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) ? (subst (λ k → FClosure A f k b) ? (init ab)) ⟫  -- b = px case,  u = px  u< osuc x 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -488,12 +488,14 @@
            ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) )
                        (subst (λ k → * a < * k ) (sym b=y) a<b ) )
            ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where
+                 m09 : b o< & A
+                 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
                  m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
-                 m07 {z} fc = ZChain.fcy<sup zc ? fc
+                 m07 {z} fc = ZChain.fcy<sup zc m09 fc
                  m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                 m08 {sup1} {z1} s<b fc = ZChain.order zc ? ?  fc
+                 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 (o<→≤ s<b) fc
                  m05 : b ≡ ZChain.supf zc b
-                 m05 = sym (ZChain.sup=u zc {_} {ab} ?
+                 m05 = sym (ZChain.sup=u zc {_} {ab} m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
                  m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 
@@ -585,14 +587,16 @@
           isupf z =  & (SUP.sup (ysup f mf ay))
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
+          y<sup : * y ≤ SUP.sup (ysup f mf ay)
+          y<sup = SUP.x<sup  (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay))
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ? )
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc)
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ? )
+          ... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u≤x (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
@@ -792,26 +796,6 @@
              ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
              ... | tri≈ ¬a b ¬c = x
              ... | tri> ¬a ¬b c = x
-             is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay psupf1 x) a ) →  b o< x  → (ab : odef A b) 
-               → HasPrev A (UnionCF A f mf ay psupf1 x) ab f ∨  IsSup A (UnionCF A f mf ay psupf1 x) ab  
-               → * a < * b  → odef ((UnionCF A f mf ay psupf1 x)) b
-             is-max {a} {b} ua b<x ab (case1 hasp) a<b = is-max-hp psupf1 x ua b<x ab hasp a<b
-             is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
-             ... | case1 b=y = ⊥-elim ( <-irr ?
-                       (subst (λ k → * a < * k ) (sym b=y) a<b ) )
-             ... | case2 y<b = m04 where 
-                 m07 : {z : Ordinal} → FClosure A f y z → z << psupf1 b
-                 m07 {z} fc = ?
-                 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (psupf1 sup1) z1 → z1 << psupf1 b
-                 m08 {sup1} {z1} s<b fc = ?
-                 m05 : b ≡ psupf1 b 
-                 m05 = ?
-                 m06 : ChainP A f mf ay psupf1 b b
-                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; supfu=u = sym m05 }
-                 m04 : odef (UnionCF A f mf ay psupf1 x) b
-                 m04 = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
-
-
           ... | case2 ¬x=sup =  no-extension -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)