# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669247318 -32400
# Node ID aeda5d0537d78910016cd03d3a2f3d8b298e3c81
# Parent  c804e302f11087b2e309a997e43b6ca577fb4438
...

diff -r c804e302f110 -r aeda5d0537d7 src/zorn.agda
--- a/src/zorn.agda	Wed Nov 23 19:30:29 2022 +0900
+++ b/src/zorn.agda	Thu Nov 24 08:48:38 2022 +0900
@@ -537,13 +537,6 @@
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
-   fc-inject : {x y : Ordinal }  →  (mf< : <-monotonic-f A f) → x o≤ z → y o≤ z → supf x o< z → supf y o< z
-      →  { wx wy  : Ordinal} →  FClosure A f (supf x) wx  →  FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y
-   fc-inject mf< x≤z y≤z sx<z sy<z = ? where
-        z53 : {x y : Ordinal } →  supf x o< supf y → FClosure A f (supf x) wx  →  wx << supf y
-        z53 = ?
-
-
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb ) 
       → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
@@ -779,7 +772,7 @@
      -- maximality of chain
      --
      --     supf is fixed for z ≡ & A , we can prove order and is-max
-     --
+     --     we have supf-unique now, it is provable in the first Tranfinte induction
 
      SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (mf< : <-monotonic-f A f)
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x
@@ -1341,7 +1334,7 @@
                      ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
                                 ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } )
 
-     ... | no lim = zc5 where
+     ... | no lim = ? where
 
           pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
           pzc {z} z<x = prev z z<x
@@ -1428,53 +1421,61 @@
           ... | tri≈ ¬a b ¬c = ?
           ... | tri> ¬a ¬b c = ?
 
-          zc5 : ZChain A f mf ay x
-          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 with trio< a x 
-               ... | tri< a<x ¬b ¬c = zc40 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 a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
-                       zc41 : omax a sa o< x
-                       zc41 = osucprev ( begin
-                           osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
-                           osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
-                           osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
-                           x ∎ ) where open o≤-Reasoning O
-                   ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
-                   sam = ZChain.supf (pzc (ob<x lim m<x)) a 
-                   zc42 : osuc a o≤ osuc m
-                   zc42 = osucc (o<→≤ ( omax-x _ _ ) )
-                   sam<m : sam o< m
-                   sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
-                   fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
-                   fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
-                   zc40 : odef (UnionCF A f mf ay supf1 b) w
-                   zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-                   ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                   ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫  where -- u o< px → u o< b ?
-                       zc55 : u o< osuc m
-                       zc55 = u<x
-                       zc56 : u ≡ supf1 a
-                       zc56 = ?
-                       u<b : u o< b --      b o≤ u → b o≤ a -- u ≡ supf1 a
-                       u<b = ?
-                       fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
-                       fc1m = fc1
-                       fc2 : FClosure A f (supf1 u) w
-                       fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) )  fc1 where
-                           zc57 : osuc u o≤ osuc m 
-                           zc57 = osucc u<x
-                       fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) w
-                       fc1a = fc
-               ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
-               ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤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 osuc-≡< b≤x
+          ... | case1 b=x with trio< a x 
+          ... | tri< a<x ¬b ¬c = zc40 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 a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
+                   zc41 : omax a sa o< x
+                   zc41 = osucprev ( begin
+                       osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
+                       osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
+                       osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
+                       x ∎ ) where open o≤-Reasoning O
+               ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
+               sam = ZChain.supf (pzc (ob<x lim m<x)) a 
+               zc42 : osuc a o≤ osuc m
+               zc42 = osucc (o<→≤ ( omax-x _ _ ) )
+               sam<m : sam o< m
+               sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
+               fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
+               fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
+               zcm : odef (UnionCF A f mf ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
+               zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
+               zc40 : odef (UnionCF A f mf ay supf1 b) w
+               zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
+               ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫  where -- u o< px → u o< b ?
+                   zc55 : u o< osuc m
+                   zc55 = u<x
+                   zc56 : u ≡ supf1 a
+                   zc56 = ?
+                   u<b : u o< b --      b o≤ u → b o≤ a -- u ≡ supf1 a
+                   u<b = ?
+                   fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
+                   fc1m = fc1
+                   fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) w
+                   fc1a = fc
+                   fc2 : FClosure A f (supf1 u) w
+                   fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) )  fc1 where
+                       zc57 : osuc u o≤ osuc m 
+                       zc57 = osucc u<x
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
+          ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
+          cfcs mf< {a} {b} {w} a<b b≤x sa<x fc | case2 b<x = zc40 where
+               zcb : odef (UnionCF A f mf ay (ZChain.supf (pzc  (ob<x lim b<x))) b) w
+               zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< ? ? ? ?
+               zc40 : odef (UnionCF A f mf ay supf1 b) w
+               zc40 with zcb
+               ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u ? ? ? ⟫  
+                 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---