# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668759347 -32400
# Node ID e18d9764365acff2488256345aec802236cdcc04
# Parent  71f231c9ed6ff0a029484d95a892e12199a81061
...

diff -r 71f231c9ed6f -r e18d9764365a src/zorn.agda
--- a/src/zorn.agda	Fri Nov 18 14:34:20 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 17:15:47 2022 +0900
@@ -430,7 +430,7 @@
       supf :  Ordinal → Ordinal
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
            → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b
-      fcs<sup : (mf< : <-monotonic-f A f)
+      cfcs : (mf< : <-monotonic-f A f)
          {a b w : Ordinal } → a o< b → b o≤ z → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
 
       asupf :  {x : Ordinal } → odef A (supf x)
@@ -441,12 +441,12 @@
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x)
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
 
-   -- fcs<sup implirs supf-mono and supf-<
+   -- cfcs implirs supf-mono and supf-<
    -- ¬ ( HasPreb A A f (supf b)
    -- supf-mono' : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
    -- supf-mono' {x} {y} x≤y with osuc-≡< x≤y
    -- ... | case1 eq = o≤-refl0 ( cong supf eq )
-   -- ... | case2 lt with fcs<sup lt ? (init asupf refl)
+   -- ... | case2 lt with cfcs lt ? (init asupf refl)
    -- ... | ⟪ ua , ch-init fc ⟫ = ?
    -- ... | ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?
 
@@ -494,7 +494,7 @@
 
    csupf : (mf< : <-monotonic-f A f) {b : Ordinal } 
       → supf b o< supf z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
-   csupf mf< {b} sb<sz = fcs<sup mf< (supf-inject sb<sz) o≤-refl (init asupf refl)
+   csupf mf< {b} sb<sz = cfcs mf< (supf-inject sb<sz) o≤-refl (init asupf refl)
 
    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)
@@ -760,7 +760,7 @@
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.fcs<sup zc mf< b<x x≤A  fc
+                          m13 = ZChain.cfcs zc mf< b<x x≤A  fc
 
         ... | no lim = record { is-max = is-max ; order = order }  where
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
@@ -798,7 +798,7 @@
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
                           m13 :  odef (UnionCF A f mf ay supf x) z
-                          m13 = ZChain.fcs<sup zc mf< b<x x≤A  fc
+                          m13 = ZChain.cfcs zc mf< b<x x≤A  fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -962,7 +962,7 @@
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; fcs<sup = ?  }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?  }  where
                  --  supf0 px is included in the chain of sp1
                  --  supf0 px ≡ px ∧ supf0 px o< sp1 → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
                  --     else                             UnionCF A f mf ay supf0 px  ≡ UnionCF supf1 x
@@ -1033,13 +1033,13 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 fcs<sup : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                      → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
-                 fcs<sup mf< {a} {b} {w} a<b b≤x fc with trio< a px
+                 cfcs mf< {a} {b} {w} a<b b≤x fc 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.fcs<sup 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) 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
@@ -1053,7 +1053,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.fcs<sup zc mf< a<px o≤-refl fc  
+                      z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl 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
@@ -1078,24 +1078,29 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
                       z51 : FClosure A f (supf1 px) w
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
+                      z53 : odef A w
+                      z53 = A∋fc {A} _ f mf fc
+                      fc1 : FClosure A f (supf1 px) w
+                      fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym (sf1=sf0 o≤-refl )) ) fc
                       csupf1 : odef (UnionCF A f mf ay supf1 b) w
                       csupf1 with trio< (supf0 px) x
-                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup (supf0 px) (subst (λ k → supf0 px o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫  where 
+                      ... | tri< sfpx<x ¬b ¬c = csupf2 where
                           -- supf0 px o< x ,   supf0 px is member of (UnionCF A f mf ay supf1 x)
-                          z53 : odef A w
-                          z53 = A∋fc {A} _ f mf fc
-                          z54 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
-                          z54 {z} ⟪ az , ch-init fc ⟫ = ?
-                          z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ?
-                          z52 : supf1 (supf0 px) ≡ supf0 px
-                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x) 
-                             ⟪ record { x≤sup = z54  } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ )
-                          fc1 : FClosure A f (supf1 (supf0 px)) w
-                          fc1 = subst (λ k → FClosure A f k w ) (trans ? (sym z52)) fc
-                          cp1 : ChainP A f mf ay supf1 (supf0 px)
-                          cp1 = record { fcy<sup = λ {z} fc → ? 
-                                   ; order =  λ {s} {z} s<u fc  → ? 
-                                   ; supu=u = z52 } 
+                          csupf2 : odef (UnionCF A f mf ay supf1 b) w
+                          csupf2 with osuc-≡< ((zc-b<x _ sfpx<x) )
+                          ... | case1 spx=px = ⟪ z53 , ch-is-sup px (subst (λ k → px o< k ) (sym b=x) px<x) cp1 fc1 ⟫  where 
+                              -- supf0 px ≡ px
+                              order : {s z1 : Ordinal} → supf1 s o< supf1 px → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
+                              order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
+                                   (trans (sym (ZChain.supf-is-minsup zc o≤-refl)) (sym (sf1=sf0 o≤-refl)) )
+                                   (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
+                                       o≤-refl (fcup fcs (o<→≤ (supf-inject0 supf1-mono ss<spx)) ) ))
+                              cp1 : ChainP A f mf ay supf1 px
+                              cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 o≤-refl)) 
+                                  ( ZChain.fcy<sup zc o≤-refl fc )
+                                       ; order =  order
+                                       ; supu=u = trans (sf1=sf0 o≤-refl)  spx=px } 
+                          ... | case2 spx<px = ⟪ z53 , ch-is-sup ? ? ? ? ⟫  
                       ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
                           -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
                           m12 : supf0 px ≡ sp1
@@ -1171,7 +1176,7 @@
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; fcs<sup = ?    }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?    }  where
 
                  --  supf0 px not is included by the chain
                  --     supf1 x ≡ supf0 px because of supfmax