# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669164938 -32400
# Node ID 6f6daf464616856892e75c0576c9ca69e46a8a1c
# Parent  66154af40f89b830a3ee1b88a341e97637b27b43
maxα

diff -r 66154af40f89 -r 6f6daf464616 src/zorn.agda
--- a/src/zorn.agda	Sun Nov 20 17:44:21 2022 +0900
+++ b/src/zorn.agda	Wed Nov 23 09:55:38 2022 +0900
@@ -1085,16 +1085,23 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
-                 --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-                 -- 
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                      → a o< b → b o≤ x → supf1 a o< x  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a px
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with zc43 (supf0 a) px
+                 ... | case2 px≤sa = z50 where
+                      a≤px : a o≤ px
+                      a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
+                      --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
+                      --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
+                      z50 : odef (UnionCF A f mf ay supf1 b) w
+                      z50 with osuc-≡< px≤sa
+                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) ? ? (subst (λ k → FClosure A f k w) ? fc)  ⟫ 
+                      ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) sa<x ⟫  ) 
+                 ... | case1 sa<px with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
                       z50 : odef (UnionCF A f mf ay supf1 b) w
                       z50 with osuc-≡< b≤x
-                      ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) ? fc  
+                      ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<px fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                       ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px )  ⟫  where -- u o< px → u o< b ?
                            u≤px : u o≤ px
@@ -1108,7 +1115,7 @@
                                    (sym (sf=eq u<x)) s<u)  
                                     (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
                                ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
-                      z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl ? fc  
+                      z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                       ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
                            u<b : u o< b
@@ -1142,14 +1149,25 @@
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
                           z52 : supf1 (supf0 px) ≡ supf0 px
-                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl ? )
+                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl (zc-b<x _ sfpx<x ) )
                           fc1 : FClosure A f (supf1 spx) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
                           order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
                           order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
                                    (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
                                    (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                       spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) )))
+                                       spx≤px ss<px (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where
+                                          ss<px : supf0 s o< px
+                                          ss<px = osucprev ( begin
+                                            osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 ( begin
+                                               s <⟨ supf-inject0 supf1-mono ss<spx ⟩
+                                               supf0 px  ≤⟨ spx≤px ⟩
+                                               px ∎ ) )) ⟩
+                                            osuc (supf1 s)  ≤⟨ osucc ss<spx ⟩
+                                            supf1 spx  ≡⟨ sf1=sf0 spx≤px  ⟩
+                                            supf0 spx  ≤⟨ ZChain.supf-mono zc spx≤px ⟩
+                                            supf0 px  ≤⟨ spx≤px ⟩
+                                            px ∎  ) where open o≤-Reasoning O
                           cp1 : ChainP A f mf ay supf1 spx
                           cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) 
                                   ( ZChain.fcy<sup zc spx≤px fc )
@@ -1318,6 +1336,9 @@
                zc00 : {z : Ordinal } → IChain A f supfz z → z o< & A
                zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
 
+          aic : {z : Ordinal } → IChain A f supfz z → odef A z
+          aic {z} ic = ?
+
           zeq : {xa xb z : Ordinal } 
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 
              → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z  
@@ -1388,15 +1409,26 @@
           ... | tri> ¬a ¬b c = ?
 
           zc5 : ZChain A f mf ay x
-          zc5 with zc43 x spu
-          zc5 | (case2 sp≤x ) =  ? where
-                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+          zc5 = ? where
+               cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                      → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
-          zc5 | (case1 x<sp ) =  ? where
-                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
+               cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a x 
+               ... | tri< a<x ¬b ¬c = ? where
+                   sa = ZChain.supf (pzc  (ob<x lim a<x)) a
+                   m =  omax a sa
+                   m<x : m o< x
+                   m<x with trio< a sa | inspect (omax a) sa
+                   ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim sa<x
+                   ... | tri≈ ¬a b ¬c | record { eq = eq } = subst ( λ k → k o< x ) ( begin
+                      sa ≡⟨ ? ⟩ 
+                      ? ≡⟨ sym eq ⟩ 
+                      _ ∎ ) ( ob<x lim sa<x ) where open ≡-Reasoning
+                   ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
+                   zc40 : odef (UnionCF A f mf ay supf1 b) w
+                   zc40 with ZChain.cfcs (pzc  (ob<x lim sa<x)) mf< ? o≤-refl ? ?
+                   ... | t = ?
+               ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
+               ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function