# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665362034 -32400
# Node ID 4541c9974e53c5cadeff67cc8b0b76e8b2f0d6d8
# Parent  5b6034ad8b9868abf3e15e5fc90adae570a77918
...

diff -r 5b6034ad8b98 -r 4541c9974e53 src/zorn.agda
--- a/src/zorn.agda	Sun Oct 09 21:51:23 2022 +0900
+++ b/src/zorn.agda	Mon Oct 10 09:33:54 2022 +0900
@@ -440,12 +440,6 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
-   supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
-   supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-minsup b≤z)) ( MinSUP.asm ( minsup b≤z ) )
-
-   -- supf-idem : {x : Ordinal } → supf x o≤ z  → supf (supf x) ≡ supf x
-   -- supf-idem {x} sx≤z = sup=u (supf∈A ?) sx≤z ?
-
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u≤z fc with MinSUP.x<sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
@@ -454,6 +448,19 @@
 
    -- ordering is not proved here but in ZChain1 
 
+   supf-idem : {x : Ordinal } → supf x o≤ z  
+       → ¬ HasPrev A (UnionCF A f mf ay supf (supf x)) (supf x) f
+       → supf (supf x) ≡ supf x
+   supf-idem {x} sx≤z ¬np = sup=u asupf sx≤z ⟪ record { x<sup = si00  } , ¬np ⟫  where
+        ms : MinSUP A (UnionCF A f mf ay supf (supf x)) 
+        ms =  minsup sx≤z  
+        mseq : supf (supf x) ≡ MinSUP.sup ( minsup sx≤z   )
+        mseq =  supf-is-minsup sx≤z
+        si00 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf x)) w → (w ≡ supf x) ∨ (w << supf x)
+        si00 {w} uw with MinSUP.x<sup ms uw
+        ... | case1 eq = case1 (subst (λ k → w ≡ k ) ? eq)
+        ... | case2 lt = case2 (subst (λ k → w << k ) ? lt)
+
 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
    supf = ZChain.supf zc
@@ -820,8 +827,8 @@
           ... | case1 eq = case2 eq
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
-          zc41 : supf0 px o≤ x →  ZChain A f mf ay x 
-          zc41 sfpx≤x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
+          zc41 : supf0 px o< x →  ZChain A f mf ay x 
+          zc41 sfpx<x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
                  --  supf0 px is included by the chain
                  --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 
@@ -998,14 +1005,15 @@
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
-                        zc21 (init asp refl ) = ⟪ asp , ch-is-sup (supf0 px) ?
-                                   record {fcy<sup = ? ; order = ? ; supu=u = ? } ? ⟫ where
-                            zc15 : supf1 px ≡ px
-                            zc15 = trans (sf1=sf0 o≤-refl ) ?
-                            zc14 : FClosure A f (supf1 px) px
-                            zc14 = init (subst (λ k → odef A k) ? asp) zc15
+                        zc21 (init asp refl ) = ⟪ asp , ch-is-sup (supf0 px) sfpx<x
+                                   record {fcy<sup = ? ; order = zc18 ; supu=u = zc15 } (init (asupf1 {supf0 px}) zc15) ⟫ where
+                            zc15 : supf1 (supf0 px) ≡ supf0 px
+                            zc15 = ?
                             zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
                             zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
+                            zc18 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) →
+                                FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px))
+                            zc18 {s} {z1} ss<sf fc = ?
                             zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
                                   FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
                             zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
@@ -1016,12 +1024,13 @@
                                 mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
                                 s<px : s o< px
                                 s<px = supf-inject0 supf1-mono ss<spx
-                                sf<px : supf0 s o< px
-                                sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) ?) ss<spx
-                                -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
+                                sf≤px : supf0 s o≤ px
+                                sf≤px = subst (λ k → supf0 s o< k ) ? (ordtrans ? sfpx<x )
                                 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
-                                csupf17 (init as refl ) = ZChain.csupf zc sf<px 
                                 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
+                                csupf17 (init as refl ) with osuc-≡< sf≤px 
+                                ... | case2 sf<px = ZChain.csupf zc sf<px 
+                                ... | case1 sf=px = ?
 
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
@@ -1057,10 +1066,10 @@
                      asm1 =  subst (λ k → odef A k ) ? ( MinSUP.asm sup1) 
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫  ) 
 
-          zc4 : ZChain A f mf ay x     --- supf px ≤ supf x
+          zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)
-          ... | tri> ¬a ¬b c = zc41 (o<→≤ c)
-          ... | tri≈ ¬a b ¬c = zc41 (o≤-refl0 (sym b))
+          ... | tri> ¬a ¬b c = zc41 c
+          ... | tri≈ ¬a b ¬c = ?
           ... | tri< a ¬b ¬c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where