# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663984377 -32400
# Node ID 1ec8c0cfc89207555ca35325eef9bedeb3f59bf4
# Parent  eaa863c4ebe8084c0ff88be7ebbb4dd4f409a896
...

diff -r eaa863c4ebe8 -r 1ec8c0cfc892 src/zorn.agda
--- a/src/zorn.agda	Tue Sep 20 10:06:23 2022 +0900
+++ b/src/zorn.agda	Sat Sep 24 10:52:57 2022 +0900
@@ -261,6 +261,12 @@
     ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
+--
+--         f (f ( ... (sup y))) f (f ( ... (sup z1)))
+--        /          |         /             |
+--       /           |        /              |
+--    sup y   <       sup z1          <    sup z2
+--           o<                      o<
 -- data UChain is total
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
@@ -351,12 +357,6 @@
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
---
---         f (f ( ... (sup y))) f (f ( ... (sup z1)))
---        /          |         /             |
---       /           |        /              |
---    sup y   <       sup z1          <    sup z2
---           o<                      o<
 
 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
@@ -372,11 +372,13 @@
       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) b f) → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
+      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
+
+      supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      supf-max : {x : Ordinal } → supf x o≤ supf z
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-      x≤supfx : {x : Ordinal } → x o≤ supf x
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
+      x≤supfx : z o≤ supf z
+
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
    f-next : {a : Ordinal} → odef chain a → odef chain (f a)
@@ -522,6 +524,23 @@
            sp1 :  {z : Ordinal } → z o≤ x  → SUP A (UnionCF A f mf ay (ZChain.supf zc) z)
            sp1 {z} z≤x = ZChain.sup zc z≤x
 
+     record MinSUP ( A B : HOD ) (z : Ordinal) : Set (Level.suc n) where
+       field
+          sup : HOD
+          asm : A ∋ sup
+          x<sup : {x : HOD} → B ∋ x → (& x)  o< z → (x ≡ sup ) ∨ (x < sup )   
+          minsup : {x sup1 : HOD} → B ∋ x → (& x) o< z  → (x ≡ sup1 ) ∨ (x < sup1 )  → sup ≤ sup1
+
+     msupP : {B : HOD} → MinSUP A B (& A)
+     msupP {B} = tf (& A) where
+         ind :  (x : Ordinal) → ((y : Ordinal) → y o< x → MinSUP A B y) → MinSUP A B x
+         ind x prev = ?
+         tf : (z : Ordinal) → MinSUP A B z
+         tf z = TransFinite {λ x → MinSUP A B x } ind z
+
+     M→S  : {B : HOD} {z : Ordinal } → (& B) o< z  → MinSUP A B z → SUP A B
+     M→S {B} lt ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = ? }
+
      --
      -- Second TransFinite Pass for maximality
      --
@@ -892,23 +911,23 @@
                  ... | tri≈ ¬a b ¬c = record { tsup = ?  ; tsup=sup = ? }
                  ... | tri> ¬a ¬b px<z = record { tsup = ? ; tsup=sup = ? }
 
-                 -- csupf1 : {b : Ordinal } → supf1 b o< z → odef (UnionCF A f mf ay supf1 z) (supf1 b) 
-                 -- csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z 
-                 --     record { fcy<sup = ZChain.fcy<sup zc (o<→≤ sb<z) ; order = order ; supu=u = ZChain.supf-idem zc }  
-                 --        (init (subst (λ k → odef A k) (sym (ZChain.supf-idem zc) asb))  (ZChain.supf-idem zc)) ⟫ where
-                 --    b<z : b o< z
-                 --    b<z = supf-inject0 (ZChain.supf-mono zc ( ordtrans<-≤ sb<z x≤supfx  ))
-                 --    asb : odef A (supf b)
-                 --    asb = supf∈A (o<→≤ b<z)
-                 --    supb : SUP A (UnionCF A f mf ay supf (supf b))
-                 --    supb = ZChain.sup zc (o<→≤ sb<z)
-                 --    supb-is-b : supf (supf b) ≡ & (SUP.sup supb)
-                 --    supb-is-b = ZChain.supf-is-sup zc (o<→≤ sb<z)
-                 --    order : {s z1 : Ordinal} → supf s o< supf (supf b) →
-                 --        FClosure A f (supf s) z1 → (z1 ≡ supf (supf b)) ∨ (z1 << supf (supf b))
-                 --    order {s} {z1} ss<ssb fs with SUP.x<sup supb ?
-                 --    ... | case1 eq = ?
-                 --    ... | case2 lt = ?
+                 csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) 
+                 csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z 
+                     record { fcy<sup = ?  ; order = order ; supu=u = ? }  
+                        (init ? ? ) ⟫ where
+                    b<x : b o< x
+                    b<x = ZChain.supf-inject zc ?
+                    asb : odef A (supf1 b)
+                    asb = ? --  ZChain.supf∈A zc ? -- (o<→≤ b<x)
+                    supb : SUP A (UnionCF A f mf ay supf1 (supf1 b))
+                    supb = ? -- ZChain.sup zc (o<→≤ sb<z)
+                    supb-is-b : supf1 (supf1 b) ≡ & (SUP.sup supb)
+                    supb-is-b = ? -- ZChain.supf-is-sup zc ? -- (o<→≤ sb<z)
+                    order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) →
+                        FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b))
+                    order {s} {z1} ss<ssb fs with SUP.x<sup supb ?
+                    ... | case1 eq = ?
+                    ... | case2 lt = ?
 
           ... | case2 px<spfx = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
                           ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where