# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667121573 -32400
# Node ID df68bb333cd076ff48d1b35966fabff9af260bf3
# Parent  d396af76c5592ba036a4a86f829d034503b06838
...

diff -r d396af76c559 -r df68bb333cd0 src/zorn.agda
--- a/src/zorn.agda	Sat Oct 29 17:26:17 2022 +0900
+++ b/src/zorn.agda	Sun Oct 30 18:19:33 2022 +0900
@@ -1424,6 +1424,8 @@
           c : Ordinal 
           c = & ( SUP.sup sp1 )
           mc = MinSUP.sup msp1
+          mc<A : mc o< & A
+          mc<A =  ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫
           c=mc : c ≡ mc
           c=mc = &iso
           z20 : mc << cf nmx mc 
@@ -1440,9 +1442,9 @@
           sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
           sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
 
-          sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+          sc<<d : {mc : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
              → supf mc << MinSUP.sup spd
-          sc<<d {mc} {asc} spd = z25 where
+          sc<<d {mc} asc spd = z25 where
                 d1 :  Ordinal
                 d1 = MinSUP.sup spd -- supf d1 ≡ d
                 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
@@ -1463,6 +1465,25 @@
                     ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  ) 
                     ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) 
 
+          smc<<d : supf mc << d
+          smc<<d = sc<<d asc spd
+
+          sz<<c : {z : Ordinal } → z o< & A → supf z <= mc 
+          sz<<c z<A = MinSUP.x<sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc)  ))
+
+          sc=c : supf mc ≡ mc
+          sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
+              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
+                   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 with  MinSUP.x<sup msp1 ?
+                   ... | case1 eq = case1 (cong (*) eq)
+                   ... | case2 lt = case2 lt
+
           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
                z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
@@ -1475,7 +1496,7 @@
                     --     supf u o< spuf c → order
 
           not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx)
-          not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd hp)  where
+          not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd hp )  where
                z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
                   →  HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx)
                   →  ⊥
@@ -1484,16 +1505,20 @@
                    y = HasPrev.y hp
                    d1 :  Ordinal
                    d1 = MinSUP.sup spd -- supf d1 ≡ d
+                   z31 :  odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx (MinSUP.sup spd))
+                   z31 = ?
                    z30 : * d1 < * (cf nmx d1)
                    z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
-                   z31 : odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx d1)
-                   z31 = ?
                    z24 : y << d1
                    z24 = subst (λ k → y <<  k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
                    z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
                    z26 with  MinSUP.x<sup spd z31
                    ... | case1 eq = case1 (cong (*) eq)
                    ... | case2 lt = case2 lt
+               --   case1 : FClosure of y
+               --   case2 : u o< supf mc
+               --   case3 : u ≡ supf mc      z31
+               --   case4 : supf mc o< u     ⊥ ( why ? )
                z25 : odef (ZChain.chain zc) (cf nmx d)
                z25 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
                    (ZChain.f-next zc 
@@ -1510,7 +1535,7 @@
           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
-          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) ) 
+          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) ) 
               ( ZChain.supf-mono zc (o<→≤ d<A ))))
 
           ss<sa : supf c o< supf (& A)