# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667271472 -32400
# Node ID 86a2bfb7222e85793a4de28ee8cd21aaf1039328
# Parent  6e126013f056ee379fe542d1bb050ae02246a6a0
supf mc = mc

diff -r 6e126013f056 -r 86a2bfb7222e src/zorn.agda
--- a/src/zorn.agda	Tue Nov 01 09:21:19 2022 +0900
+++ b/src/zorn.agda	Tue Nov 01 11:57:52 2022 +0900
@@ -79,6 +79,10 @@
 <-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
 <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 
+ftrans<=-< : {x y z : Ordinal } →  x <=  y →  y << z →  x <<  z 
+ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) ? y<z
+ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z 
+
 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y 
 <=to≤ (case1 eq) = case1 (cong (*) eq)
 <=to≤ (case2 lt) = case2 lt
@@ -1501,11 +1505,16 @@
               is-sup :  IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
               is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )} 
               not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx)
-              not-hasprev hp = <-irr z26 z30 where
+              not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ?
+              not-hasprev record { ax = ax ; y = y ; ay =   ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where
                    z30 : * mc < * (cf nmx mc)
                    z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
-                   z26 : (* (cf nmx mc) ≡ * mc) ∨ (* (cf nmx mc) < * mc)
-                   z26 = ?
+                   z31 : ( supf mc ≡  mc ) ∨ ( * (supf mc) < * mc )
+                   z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
+                   z32 : * (supf mc) < * (cf nmx (cf nmx y))
+                   z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
+                   z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
+                   z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
 
           is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
           is-sup = record { x≤sup = z22 } where
@@ -1542,20 +1551,14 @@
                     z56 eq = cong supf eq
                     z57 : u << mc → supf u o≤ supf mc
                     z57 lt = ZChain.supf-<= zc (case2 z58) where
-                        z58 : supf u << supf mc -- supf u o< supf d
-                        z58 = ?
-                        z59 : supf mc o< supf u → ⊥  → supf mc << supf u
-                        z59 lt = ?
-                -- --with z52
-                -- ... | case1 eq = ?
-                -- ... | case2 lt = ? -- ZChain.supf-<= zc (case2 ? )
+                        z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
+                        z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt 
                 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
                 z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc  _ fc ))
                 z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) )
                 z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc  _ fc ))
                 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
-                    → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
-                    → supf mc << d1 
+                    → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1 
                     →  * (cf nmx (cf nmx y)) < * d1
                 z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq))  smc<d 
                 z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d
@@ -1588,6 +1591,9 @@
           ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
           ... | case2 lt = lt
 
+          ¬sms=sa : ¬ ( supf mc ≡ supf (& A)) --  → supf mc ≡  supf d ≡ supf (& A), supf mc << d
+          ¬sms=sa = ?
+
           sms<sa : supf mc o< supf (& A)
           sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
           ... | case2 lt = lt