# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667312190 -32400
# Node ID 05f54e16f138411a2511edc5976cb38ff03aa098
# Parent  86a2bfb7222e85793a4de28ee8cd21aaf1039328
z04 done

diff -r 86a2bfb7222e -r 05f54e16f138 src/zorn.agda
--- a/src/zorn.agda	Tue Nov 01 11:57:52 2022 +0900
+++ b/src/zorn.agda	Tue Nov 01 23:16:30 2022 +0900
@@ -1408,6 +1408,16 @@
                ... | case1 eq = ¬b eq
                ... | case2 lt = ¬a lt
 
+     tri : {n : Level} (u w : Ordinal ) { R : Set n }  → ( u o< w → R ) → ( u ≡  w → R ) → ( w o< u → R ) → R
+     tri {_} u w p q r with trio< u w
+     ... | tri< a ¬b ¬c = p a
+     ... | tri≈ ¬a b ¬c = q b
+     ... | tri> ¬a ¬b c = r c
+
+     or : {n m r : Level } {P : Set n } {Q : Set m} {R : Set r}  → P ∨ Q → ( P → R ) → (Q → R ) → R
+     or (case1 p) p→r q→r = p→r p
+     or (case2 q) p→r q→r = q→r q
+
 
      -- ZChain contradicts ¬ Maximal
      --
@@ -1505,7 +1515,12 @@
               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 record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ?
+              not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where 
+                   z30 : * mc < * (cf nmx mc)
+                   z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
+                   z31 : ( * (cf nmx mc)  ≡  * mc ) ∨ ( * (cf nmx mc) < * mc )
+                   z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k →  odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) 
+                       ⟪ proj2  (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc))  ⟫ ))
               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))
@@ -1518,23 +1533,44 @@
 
           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)
-               z23 lt = MinSUP.x≤sup spd lt
-               z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
+                z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
+                z23 lt = MinSUP.x≤sup spd lt
+                z22 :  {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →
                    (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd)
-               z22 {a} ⟪ aa , ch-init fc ⟫ = ?
-               z22 {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ?
+                z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where
+                    z32 : ( a  ≡  supf mc ) ∨ ( * a < * (supf mc) )
+                    z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc
+                z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc)
+                       z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where
+                    z53 : supf u o< supf (& A)
+                    z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
+                    z52 : ( u ≡ mc ) ∨  ( u << mc )
+                    z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) 
+                           , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
+                    z56 : u ≡ mc → supf u ≡  supf mc
+                    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 -- supf u << supf d
+                        z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c)  lt 
+                    z51 : supf u o≤ supf mc
+                    z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 
+                    z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d )
+                    z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A 
+                        (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1))  u<smc)  fc ) smc<<d )
+                    z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d )
+                    z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) )
                     -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
                     --     supf u o< spuf c → order
 
-          z43 : (u w : Ordinal ) → ( u o< w ) ∨ ( u ≡  w ) ∨ ( w o< u )
-          z43 u w with trio< u w
-          ... | tri< a ¬b ¬c = case1 a
-          ... | tri≈ ¬a b ¬c = case2 (case1 b)
-          ... | tri> ¬a ¬b c = case2 (case2 c) 
-
           not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) d (cf nmx)
-          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-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where 
+                z30 : * d < * (cf nmx d)
+                z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))
+                z32 : ( cf nmx (cf nmx y)  ≡  supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) )
+                z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc))
+                z31 : ( * (cf nmx d)  ≡  * d ) ∨ ( * (cf nmx d) < * d )
+                z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) ))
           not-hasprev record { ax = ax ; y = y ; ay =   ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where
                 z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
                 z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p
@@ -1546,7 +1582,7 @@
                 z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) 
                         , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
                 z51 : supf u o≤ supf mc
-                z51 = ? where
+                z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where
                     z56 : u ≡ mc → supf u ≡  supf mc
                     z56 eq = cong supf eq
                     z57 : u << mc → supf u o≤ supf mc
@@ -1565,7 +1601,7 @@
                 z30 : * d < * (cf nmx d)
                 z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))
                 z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
-                z46 = ? where
+                z46 = or (osuc-≡< z51) z55 z54 where
                    z55  : supf u ≡  supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
                    z55 eq = <=to≤  (MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j (cf nmx k) ) eq (sym x=fy ) (fsuc _ (fsuc _ fc)) ) )
                    z54  : supf u o< supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
@@ -1574,15 +1610,6 @@
                 -- ... | case1 eq =  MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup1) eq) refl fc )
                 -- ... | case2 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 ))
 
--- ax      : odef A d
--- y       : Ordinal
--- ua1     : odef A y
--- u       : Ordinal
--- u<x     : supf u o< supf d
--- is-sup1 : ChainP A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf u
--- fc      : FClosure A (cf nmx) (supf u) y
--- x=fy    : d ≡ cf nmx y
-
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
 
@@ -1591,9 +1618,6 @@
           ... | 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