# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665496033 -32400
# Node ID d917831fb60744870f2a92c4104db2f2fce266ac
# Parent  a6f075a164fa7e0ff9d39fd1710e538641644a9d
  supf (supf x) ≡ supf x  is bad

diff -r a6f075a164fa -r d917831fb607 src/zorn.agda
--- a/src/zorn.agda	Tue Oct 11 10:41:19 2022 +0900
+++ b/src/zorn.agda	Tue Oct 11 22:47:13 2022 +0900
@@ -385,6 +385,14 @@
    ... | case2 lt = case2 (subst₂ (λ j k →  j < k ) *iso refl lt )
 
 
+chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 
+   {a b c : Ordinal} → a o≤ b
+        → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
+chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
+        ⟪ ua , ch-init fc  ⟫ 
+chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
+        ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫ 
+
 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
@@ -411,7 +419,7 @@
 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
-   f-next : {a : Ordinal} → odef chain a → odef chain (f a)
+   f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a)
    f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
    f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
    initial : {z : Ordinal } → odef chain z → * y ≤ * z
@@ -448,7 +456,21 @@
 
    -- ordering is not proved here but in ZChain1 
 
-   -- supf-idem : {x : Ordinal } → supf x o< z  → supf (supf x) ≡ supf x
+   supf-¬hp : {x : Ordinal } → x o≤ z → odef (UnionCF A f mf ay supf x) (supf x)
+       → ( supf x ≡ f (supf x) ) ∨  ( ¬  HasPrev A chain (supf x) f )
+   supf-¬hp {x} x≤z usx with proj1 ( mf (supf x) asupf )
+   ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) eq)) 
+   ... | case2 s<fs = case2 sh00 where
+       sh00 : ( ¬  HasPrev A chain (supf x) f )
+       sh00 hp = <-irr (<=to≤ sh01) s<fs where
+          sh01 : ( f ( supf x ) ≡  supf x ) ∨  ( f ( supf x ) <<  supf x )
+          sh01 = subst (λ k → ( f ( supf x ) ≡  k ) ∨  ( f ( supf x ) << k )) (sym (supf-is-minsup x≤z)) 
+              ( MinSUP.x<sup ( minsup x≤z ) (f-next usx )) 
+
+   supf-idem : {x : Ordinal } → supf x o< z  → supf (supf x) ≡ supf x
+   supf-idem {x} sf<z with csupf sf<z
+   ... | ⟪ au , ch-init fc ⟫ = ? 
+   ... | ⟪ au , ch-is-sup u u<z is-sup fc ⟫ = ?
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -566,14 +588,6 @@
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
-     chain-mono :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 
-       {a b c : Ordinal} → a o≤ b
-            → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
-     chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
-            ⟪ ua , ch-init fc  ⟫ 
-     chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫ 
-
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
      sp0 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
@@ -1079,6 +1093,8 @@
                      --  z1 ≡ px , supf0 px ≡  px
                      psz1≤px :  supf1 z1 o≤ px
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
+                     cs00 : supf1 (supf1 px) ≡ supf1 px
+                     cs00 = ?
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                      csupf2 with  trio< z1 px | inspect supf1 z1
                      csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
@@ -1086,24 +1102,29 @@
                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
                           -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px
                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
-                          supu=u = ?
+                          supu=u = ? -- ZChain.sup=u zc ? ? ?
                      ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
                      ... | ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫
                      ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , 
                                ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) 
-                                 record { fcy<sup = ? ; order = ? ; supu=u = ?  } (fcpu fc (o<→≤ u<x))  ⟫ 
+                                 record { fcy<sup = ? ; order = ? ; supu=u = ?  } (fcpu fc (o<→≤ u<x))  ⟫  where
+                          supu=u : supf1 (supf1 z1) ≡ supf1 z1
+                          supu=u = ? -- ZChain.sup=u zc ? ? ?
                      csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
                           -- supf1 z1 ≡ supf0 z1, z1 ≡ px
-                          asm : odef A (supf1 z1)
-                          asm =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
-                          asm1 : odef A (supf1 (supf1 z1))
-                          asm1 =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
                           supu=u = ?
                      csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
                           --  supf1 z1 ≡ sp1, px o< z1
+                          asm : odef A (supf1 z1)
+                          asm =  subst (λ k → odef A k ) (sym (sf1=sp1 c)) ( MinSUP.asm sup1) 
+                          sp1=px : sp1 ≡ px
+                          sp1=px with trio< sp1 px
+                          ... | tri> ¬a ¬b c = ?
+                          ... | tri≈ ¬a b ¬c = b
+                          ... | tri< a ¬b ¬c = ?
                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
                           supu=u = ?