# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669187571 -32400
# Node ID 2362c2d89d3623edebdb4c1ca773309f770a3090
# Parent  6f6daf464616856892e75c0576c9ca69e46a8a1c
fc-inject is no good

diff -r 6f6daf464616 -r 2362c2d89d36 src/zorn.agda
--- a/src/zorn.agda	Wed Nov 23 09:55:38 2022 +0900
+++ b/src/zorn.agda	Wed Nov 23 16:12:51 2022 +0900
@@ -511,6 +511,12 @@
        fsp≤sp : f sp <=  sp
        fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
 
+   supf-¬hp : {x  : Ordinal } → x o≤ z 
+       → ( {a : Ordinal } → odef A a → a << f a )
+       → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f (supf x) )
+   supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → 
+       (subst (λ k → w <= k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
+
    supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
    supf-idem  mf< {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
@@ -525,10 +531,19 @@
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
-spuf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
+   fc-inject :    ( {a : Ordinal } → odef A a → a << f a )
+      →  {x y wx wy  : Ordinal} →  FClosure A f (supf x) wx  →  FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y
+   fc-inject mf< (init xa eqa) (init ya eqb) refl = trans eqa (sym eqb)
+   fc-inject mf< {x} (init xa eqx) (fsuc ya fcy) eq = ⊥-elim ( supf-¬hp ? mf< record { ax = asupf ; y = ya ; ay = ? ; x=fy = trans eqx eq } ) where
+        z53 : odef (UnionCF A f mf ay supf x) ya
+        z53 = cfcs ? ? ? ? fcy
+   fc-inject mf< (fsuc xa fcx) (init ya eqy) eq = ?
+   fc-inject mf< (fsuc xa fcx) (fsuc ya fcy) eq = fc-inject mf< fcx fcy ? 
+
+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
-spuf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
+supf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
        supfa = ZChain.supf za
        supfb = ZChain.supf zb
        ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
@@ -597,6 +612,7 @@
                         z55 : FClosure A f (ZChain.supf zb u) z
                         z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
 
+
 UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
         → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
@@ -1342,7 +1358,7 @@
           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  
-          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  spuf-unique A f mf ay xa≤xb  
+          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf ay xa≤xb  
               (pzc xa<x)  (pzc xb<x)  z≤xa
 
           ptotalx : IsTotalOrderSet pchainx
@@ -1413,20 +1429,41 @@
                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 = ? where
+               ... | 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 b ¬c | record { eq = eq } = subst ( λ k → k o< x ) ( begin
-                      sa ≡⟨ ? ⟩ 
-                      ? ≡⟨ sym eq ⟩ 
-                      _ ∎ ) ( ob<x lim sa<x ) where open ≡-Reasoning
+                   ... | 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 sa<x)) mf< ? o≤-refl ? ?
-                   ... | t = ?
+                   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 = ?
                ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
                ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))