Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 950:6e126013f056

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 01 Nov 2022 09:21:19 +0900
parents efc833407350
children 86a2bfb7222e
files src/zorn.agda
diffstat 1 files changed, 73 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 31 23:27:55 2022 +0900
+++ b/src/zorn.agda	Tue Nov 01 09:21:19 2022 +0900
@@ -238,13 +238,13 @@
 
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
    field
-      x<sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+      x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
       as : A ∋ sup
-      x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
+      x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
 --
 --  sup and its fclosure is in a chain HOD
@@ -365,7 +365,7 @@
    field
       sup : Ordinal
       asm : odef A sup
-      x<sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup )   
+      x≤sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup )   
       minsup : { sup1 : Ordinal } → odef A sup1 
          →  ( {x : Ordinal  } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 ))  → sup o≤ sup1
 
@@ -377,10 +377,10 @@
       →  MinSUP A (UnionCF A f mf ay supf x)  
       → SUP A (UnionCF A f mf ay supf x) 
 M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms) 
-        ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm ms) ; x<sup = ms00 } where
+        ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm ms) ; x≤sup = ms00 } where
    msup = MinSUP.sup ms
    ms00 : {z : HOD} → UnionCF A f mf ay supf x ∋ z → (z ≡ * msup) ∨ (z < * msup)
-   ms00 {z} uz with MinSUP.x<sup ms uz 
+   ms00 {z} uz with MinSUP.x≤sup ms uz 
    ... | case1 eq = case1 (subst (λ k → k ≡ _) *iso ( cong (*) eq))
    ... | case2 lt = case2 (subst₂ (λ j k →  j < k ) *iso refl lt )
 
@@ -452,7 +452,7 @@
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
    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)  
+   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)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
    ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
@@ -535,7 +535,7 @@
                 ... | tri< a ¬b ¬c with prev z a
                 ... | case2 mins = case2 mins
                 ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z)
-                ... | case1 mins = case2 record { sup = z ; asm = proj1 mins ; x<sup = proj2 mins ; minsup = m04 } where
+                ... | case1 mins = case2 record { sup = z ; asm = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } where
                   m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1
                   m04 {s} as lt with trio< z s
                   ... | tri< a ¬b ¬c = o<→≤ a
@@ -548,7 +548,7 @@
              S = supP B  B⊆A total
              s1 = & (SUP.sup S)
              m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 )
-             m05 {w} bw with SUP.x<sup S {* w} (subst (λ k → odef B k) (sym &iso) bw )
+             m05 {w} bw with SUP.x≤sup S {* w} (subst (λ k → odef B k) (sym &iso) bw )
              ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) eq) )
              ... | case2 lt = case2 ( subst (λ k → _ < k ) (sym *iso) lt )
          m02 : MinSUP A B 
@@ -623,7 +623,7 @@
         order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
         order {b} {s} {z1} b<z ss<sb fc = zc04 where
           zc00 : ( z1  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
-          zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc ))
+          zc00 = MinSUP.x≤sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc ))
           -- supf (supf b) ≡ supf b
           zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
           zc04 with zc00
@@ -653,7 +653,7 @@
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz) }  , m04 ⟫
+                      ⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz) }  , m04 ⟫
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -668,7 +668,7 @@
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b 
-           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
+           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSup.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
            ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
@@ -686,7 +686,7 @@
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫    -- ZChain on x
+                      ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -705,7 +705,7 @@
      ysup f mf {y} ay = minsupP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
-     SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
+     SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt)    }
 
      record xSUP (B : HOD) (x : Ordinal) : Set n where
         field
@@ -774,7 +774,7 @@
                     zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
                     ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
                     ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
-                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) 
+                    zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) 
                        (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
                     ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
                     ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) 
@@ -839,7 +839,7 @@
                        zc21 : MinSUP A (UnionCF A f mf ay supf0 a)
                        zc21 = ZChain.minsup zc (o<→≤ a<px)
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) )
+                       zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) )
                        zc19 : supf0 a o≤ sp1 
                        zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
@@ -848,7 +848,7 @@
                        zc20 : MinSUP.sup zc21 ≡ supf0 a
                        zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) 
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
-                       zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
+                       zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
                        zc18 : supf0 a o≤ sp1 
                        zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
@@ -943,7 +943,7 @@
                               zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
                                     FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
                               zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
-                                     (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
+                                     (MinSUP.x≤sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
                                   mins : MinSUP A (UnionCF A f mf ay supf0 px)
                                   mins = ZChain.minsup zc o≤-refl
                                   mins-is-spx : MinSUP.sup mins ≡ supf1 px 
@@ -985,26 +985,26 @@
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px 
                  ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
+                         ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
                     ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {x} ux = MinSUP.x<sup m ?
+                    ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m ? ?
                  ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m  
-                         ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
+                         ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
                     ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {x} ux = MinSUP.x<sup m ?
+                    ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m ? ?
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
-                         ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
+                         ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
                     m = sup1
                     ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {x} ux = MinSUP.x<sup m ?
+                    ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m ? ?
@@ -1111,9 +1111,9 @@
                         s1u=x = trans ? eq
                         zc13 : osuc px o< osuc u1
                         zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) 
-                        x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
-                        x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
-                        x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? ))
+                        x≤sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
+                        x≤sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
+                        x≤sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? ))
                         ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where
                                  zc14 : u ≡ osuc px
                                  zc14 = begin
@@ -1127,7 +1127,7 @@
                         zc12 = subst  (λ k → supf0 k ≡ u1) eq ?
                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                         zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
-                                 ; is-sup = record { x<sup = x<sup } }
+                                 ; is-sup = record { x≤sup = x≤sup } }
                  zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
@@ -1163,24 +1163,24 @@
                      zc32 = ZChain.sup zc o≤-refl 
                      zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
                      zc34 ne {w} lt with zc11 ? ⟪ proj1 lt , ? ⟫
-                     ... | case1 lt = SUP.x<sup zc32 lt 
+                     ... | case1 lt = SUP.x≤sup zc32 lt 
                      ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
                      zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
-                     zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  } 
+                     zc36 ne = ? -- record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x≤sup = zc34 ne } ; tsup=sup = zc33  } 
                      zc35 : STMP z≤x
                      zc35 with trio< (supf0 px) px
                      ... | tri< a ¬b ¬c = zc36 ¬b
                      ... | tri> ¬a ¬b c = zc36 ¬b
                      ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
                           zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
-                          zc37 = record { sup = ? ; asm = ? ; x<sup = ? }
+                          zc37 = record { sup = ? ; asm = ? ; x≤sup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ 
                  ... | tri> ¬a ¬b px<b = zc31 ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -1188,8 +1188,8 @@
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                      zcsup with zc30
-                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
-                        IsSup.x<sup (proj1 is-sup) ?} } 
+                     ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt → 
+                        IsSup.x≤sup (proj1 is-sup) ?} } 
                      zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
                      zc31 (case1 ¬sp=x) with zc30
                      ... | refl = ⊥-elim (¬sp=x zcsup )
@@ -1283,8 +1283,8 @@
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
                  sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
                  sup=u {z} ab z≤x is-sup with trio< z x
-                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }
+                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x≤sup = {!!} }
+                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x≤sup = {!!} }
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
 
           zc5 : ZChain A f mf ay x 
@@ -1367,21 +1367,21 @@
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z22 : sp o< & A
            z22 = z09 asp
-           x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
-           x<sup bz = SUP.x<sup sp1 bz 
+           x≤sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
+           x≤sup bz = SUP.x≤sup sp1 bz 
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
            ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
-               z13 with x<sup ( ZChain.chain∋init zc )
+               z13 with x≤sup ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
                z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
-               z19 = record {   x<sup = z20 }  where
+               z19 = record {   x≤sup = z20 }  where
                    z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
-                   z20 {y} zy with x<sup (subst (λ k → odef chain k ) (sym &iso) zy)
+                   z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy)
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
            ztotal : IsTotalOrderSet (ZChain.chain zc)
@@ -1398,7 +1398,7 @@
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
                z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  SUP.sup sp1 )
-               z15  = x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z15  = x≤sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
@@ -1450,7 +1450,7 @@
                 d1 :  Ordinal
                 d1 = MinSUP.sup spd -- supf d1 ≡ d
                 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
-                z24 = MinSUP.x<sup spd (init asc refl)
+                z24 = MinSUP.x≤sup spd (init asc refl)
                 --
                 --   f ( f .. ( supf mc ) <= d1
                 --   f d1 <= d1
@@ -1461,7 +1461,7 @@
                 ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
                     --  supf mc ≡ d1
                     z32 : ((cf nmx (supf mc)) ≡ d1) ∨ ( (cf nmx (supf mc)) << d1 )
-                    z32 = MinSUP.x<sup spd (fsuc _ (init asc refl))
+                    z32 = MinSUP.x≤sup spd (fsuc _ (init asc refl))
                     z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
                     z29  with z32
                     ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  ) 
@@ -1473,7 +1473,7 @@
                 d1 :  Ordinal
                 d1 = MinSUP.sup spd -- supf d1 ≡ d
                 z24 : (z ≡ d1) ∨ ( z << d1 )
-                z24 = MinSUP.x<sup spd fc
+                z24 = MinSUP.x≤sup spd fc
                 --
                 --   f ( f .. ( supf mc ) <= d1
                 --   f d1 <= d1
@@ -1484,7 +1484,7 @@
                 ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
                     --  supf mc ≡ d1
                     z32 : ((cf nmx z) ≡ d1) ∨ ( (cf nmx z) << d1 )
-                    z32 = MinSUP.x<sup spd (fsuc _ fc)
+                    z32 = MinSUP.x≤sup spd (fsuc _ fc)
                     z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
                     z29  with z32
                     ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  ) 
@@ -1494,12 +1494,12 @@
           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)  ))
+          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 )} 
+              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)
@@ -1508,9 +1508,9 @@
                    z26 = ?
 
           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
+          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
+               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 ⟫ = ?
@@ -1534,10 +1534,19 @@
                 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) 
+                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 = ? --with z52
+                z51 = ? where
+                    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
+                        z58 = ?
+                        z59 : supf mc o< supf u → ⊥  → supf mc << supf u
+                        z59 lt = ?
+                -- --with z52
                 -- ... | case1 eq = ?
                 -- ... | case2 lt = ? -- ZChain.supf-<= zc (case2 ? )
                 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
@@ -1545,12 +1554,22 @@
                 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)) < * d1
-                z47 {mc} {d1} {asc} spd = ?
+                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
                 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 = z45 (case2 (z47 {mc} {d} {asc} spd  ))
+                z46 = ? 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)
+                   z54 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 ))
+                -- z46 with osuc-≡< z51
+                -- ... | 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