Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 979:6229017a6176

chain is now u≤x again

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 09 Nov 2022 05:00:56 +0900
parents	94357ced682d
children	49cf50d451e1

comparison

equal deleted inserted replaced

-:94357ced682d
+:6229017a6176
 supu=u   : supf u ≡ u
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where
 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u )
+ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u≤x : supf u o≤ supf 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
+--    sup y   ≤       sup z1          ≤    sup z2
---           o<                      o<
+--           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 )
 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
 ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca
+ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca
 ... | case1 eq with s≤fc (supf ub) f mf fcb
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * a ≡ * b
 ct00 = trans (cong (*) eq) eq1
 ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
 ct01 : * a < * b
 ct01 = subst (λ k → * k < * b ) (sym eq) lt
-ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
 ct00 : * a < * (supf ub)
 ct00 = lt
 ct01 : * a < * b
 ct01 with s≤fc (supf ub) f mf fcb
 ... | case1 eq =  subst (λ k → * a < k ) eq ct00
 ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
+ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
 ... | case1 eq with s≤fc (supf ua) f mf fca
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * a ≡ * b
 ct00 = sym (trans (cong (*) eq) eq1 )
 ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
 ct01 : * b < * a
 ct01 = subst (λ k → * k < * a ) (sym eq) lt
-ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
 ct00 : * b < * (supf ua)
 ct00 = lt
 ct01 : * b < * a
 ct01 with s≤fc (supf ua) f mf fca
 ... | case1 eq =  subst (λ k → * b < k ) eq ct00
 (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
 → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ =
 ⟪ ua , ch-init fc  ⟫
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ =
-⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (supf-mono a≤b ) ) is-sup fc  ⟫
+⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x ? ) is-sup fc  ⟫
 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
 field
 supf :  Ordinal → Ordinal
 chain∋init : odef chain y
 chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
 f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a)
 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-f-next {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x is-sup (fsuc _ fc ) ⟫
+f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
 initial : {z : Ordinal } → odef chain z → * y ≤ * z
 initial {a} ⟪ aa , ua ⟫  with  ua
 ... | ch-init fc = s≤fc y f mf fc
-... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
+... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
 zc7 : y <= supf u
 zc7 = ChainP.fcy<sup is-sup (init ay refl)
 f-total : IsTotalOrderSet chain
 f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
 → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x)
 → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x)
 → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z
 UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫  where
+UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u≤x is-sup fc ⟫ = ⟪ az , ch-is-sup u ? cp1 fc1 ⟫  where
-u<x0 : u o< z
+u≤x0 : u o< z
-u<x0 = supf-inject0 supf-mono u<x
+u≤x0 = supf-inject0 supf-mono ?
-u<x1 : supf1 u o< supf1 z
+u≤x1 : supf1 u o< supf1 z
-u<x1 = subst (λ k → k o< supf1 z ) (eq<x u<x0) (ordtrans<-≤ u<x (lex o≤-refl ) )
+u≤x1 = subst (λ k → k o< supf1 z ) (eq<x u≤x0) (ordtrans<-≤ u≤x ? ) -- (lex o≤-refl ) )
 fc1 : FClosure A f (supf1 u) x
-fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x0) fc
+fc1 = subst (λ k → FClosure A f k x ) (eq<x u≤x0) fc
 uc01 : {s : Ordinal } →  supf1 s o< supf1 u → s o< z
 uc01 {s} s<u with trio< s z
 ... | tri< a ¬b ¬c = a
-... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02  s<u ) where -- (supf-mono (o<→≤ u<x0))
+... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02  s<u ) where -- (supf-mono (o<→≤ u≤x0))
 uc02 :  supf1 u o≤ supf1 s
 uc02 = begin
-supf1 u  <⟨ u<x1 ⟩
+supf1 u  <⟨ u≤x1 ⟩
 supf1 z  ≡⟨ cong supf1 (sym b) ⟩
 supf1 s ∎  where open o≤-Reasoning O
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> uc03 s<u ) where
 uc03 :  supf1 u o≤ supf1 s
 uc03 = begin
-supf1 u  ≡⟨ sym (eq<x u<x0) ⟩
+supf1 u  ≡⟨ sym (eq<x u≤x0) ⟩
-supf u  <⟨ u<x ⟩
+supf u  <⟨ ? ⟩
 supf z  ≤⟨ lex (o<→≤ c) ⟩
 supf1 s ∎  where open o≤-Reasoning O
 cp1 : ChainP A f mf ay supf1 u
-cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0) (ChainP.fcy<sup is-sup fc )
+cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u≤x0) (ChainP.fcy<sup is-sup fc )
-; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0)
+; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u≤x0)
-(ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x0)) s<u)
+(ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u≤x0)) s<u)
 (subst (λ k → FClosure A f k z ) (sym (eq<x (uc01 s<u) )) fc ))
-; supu=u = trans (sym (eq<x u<x0)) (ChainP.supu=u is-sup)  }
+; supu=u = trans (sym (eq<x u≤x0)) (ChainP.supu=u is-sup)  }
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 supf = ZChain.supf zc
 field
 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b)
 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b
 → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev
 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
-... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
+... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
-(sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
+(sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫
 supf = ZChain.supf zc
 csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
 csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
 zc05 with zc04
 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
-... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where
+... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where
 zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
 zc07 = fc
 zc06 : supf u ≡ u
 zc06 = ChainP.supu=u is-sup
 zc08 : supf u o< supf b
 zc08 = ordtrans≤-< (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc ))) ss<sb
 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
 zc04 : odef (UnionCF A f mf ay supf b) (f x)
 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
-... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫
+... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
 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 ))
 -- supf (supf b) ≡ supf b
 HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
 is-max {a} {b} ua b<x 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
-= ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+= ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
 b<A : b o< & A
 b<A = z09 ab
 b<x : b o< x
 b<x  = ZChain.supf-inject zc sb<sx
 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
 * 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 )
 ... | 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
+... | case2 y<b = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 b<x : b o< x
 b<x  = ZChain.supf-inject zc sb<sx
 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
 zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
-u<x :  u o< x
+u≤x :  u o< x
-u<x =  supf-inject0 supf1-mono su<sx
+u≤x =  supf-inject0 supf1-mono ? -- su<sx
 u≤px : u o≤ px
-u≤px = zc-b<x _ u<x
+u≤px = zc-b<x _ u≤x
 zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
 zc21 {z1} (fsuc z2 fc ) with zc21 fc
 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
+... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫
 ... | case2 fc = case2 (fsuc _ fc)
 zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u
-... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
+... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17
 ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
 u<px :  u o< px
 u<px =  ZChain.supf-inject zc a
 asp0 : odef A (supf0 u)
 asp0 = ZChain.asupf zc
 zc18 : s o≤ px
 zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px
 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc )
 ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b )))
-... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x  ⟫ )
 zc35 : {z : Ordinal} → ¬ (supf0 px ≡ px) → odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
 zc35 {z} ne ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫
-zc35 {z} ne ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) )
+zc35 {z} ne ⟪ ua1 , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono ?)) )
 ... | case1 eq = zc34 where
-u<x0 : u o≤ px
+u≤x0 : u o≤ px
-u<x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono u<x )
+u≤x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono ? )
 zc34 : odef (UnionCF A f mf ay supf0 x) z
 zc34 with trio< (supf0 px) px
 ... | tri< sf0px<px ¬b ¬c = cp3 ( subst ( λ k → FClosure A f k z)
-(trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where
+(trans (trans (sf1=sf0 u≤x0) eq) (ZChain.supfmax zc px<x) ) fc) where
 cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z
 cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px)
 cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc)
 ... | tri≈ ¬a b ¬c = ⊥-elim (ne b)
 ... | tri> ¬a ¬b px<sf0px = ⊥-elim (¬p<x<op ⟪ cp5 , cp4 ⟫ ) where
 cp4 : u o< osuc px
-cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono u<x  )
+cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono ?  )
 cp5 : px o< u
 cp5 = subst (λ k → px o< k ) ( begin
 supf0 px ≡⟨ sym (ZChain.supfmax zc px<x)  ⟩
 supf0 x  ≡⟨ sym eq  ⟩
-supf0 u  ≡⟨ sym (sf1=sf0 u<x0)  ⟩
+supf0 u  ≡⟨ sym (sf1=sf0 u≤x0)  ⟩
 supf1 u  ≡⟨ ChainP.supu=u is-sup  ⟩
 u ∎  ) px<sf0px  where open ≡-Reasoning
-... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where
+... | case2 u≤x1 = ⟪ ua1 , ch-is-sup u ? cp1 fc1 ⟫ where
-u<x0 : u o< x
+u≤x0 : u o< x
-u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤  px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px
+u≤x0 = supf-inject0 supf1-mono ? -- supf0 u o≤  px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px
 sf0u=sf1u : supf0 u ≡ supf1 u
-sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))
+sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 ))
 cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s
 cp2 {s} ss<su = sym ( sf1=sf0 ( begin
 s  <⟨ ZChain.supf-inject zc ss<su ⟩
-u  ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0  ⟩
+u  ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0  ⟩
 px ∎ )) where open o≤-Reasoning O
 fc1 : FClosure A f (supf0 u) z
 fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc
 cp1 : ChainP A f mf ay supf0 u
 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc )
 ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u)
 (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u)
 (subst (λ k → FClosure A f k z ) (cp2 s<u) fc ))
-; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup)  }
+; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 ))) (ChainP.supu=u is-sup)  }
 zc33 : {z : Ordinal} → ¬ (supf0 px o< sp1) → odef (UnionCF A f mf ay supf1 x) z  → odef (UnionCF A f mf ay supf0 x) z
 zc33 {z} lt = UChain⊆ A f mf ay supf1-mono (λ lt → sym (sf=eq lt)) sf≤0  where
 sf≤0 :  { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z
 sf≤0 {z} x≤z with trio< z px
 zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
 u<px :  u o< px
-u<px = ZChain.supf-inject zc su<sx
+u<px = ZChain.supf-inject zc ? -- su<sx
-u<x : u o< x
+u≤x : u o< x
-u<x = ordtrans u<px px<x
+u≤x = ordtrans u<px px<x
 u≤px : u o≤ px
 u≤px = o<→≤ u<px
 s1u<s1x : supf1 u o< supf1 x
-s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) su<sx) (supf1-mono (o<→≤ px<x) )
+s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) ?) (supf1-mono (o<→≤ px<x) )
 zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1
 zc21 {z1} (fsuc z2 fc ) with zc21 fc
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫
 zc21 (init asp refl ) with trio< u px | inspect supf1 u
 ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u
-s1u<s1x
+? -- s1u<s1x
 record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (ChainP.supu=u is-sup) } zc14 ⟫  where
 zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
 zc17 {s} {z1} ss<su fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<px))) ( ChainP.order is-sup
 (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<px)) ss<su) (fcup fc s≤px) ) where
 s≤px = ordtrans ( supf-inject0 supf1-mono ss<su ) (o<→≤ u<px)
 zc14 : FClosure A f (supf1 u) (supf0 u)
 zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px)
 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 u≤px )) ( ChainP.fcy<sup is-sup fc )
-... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (subst (λ k → supf1 k o< supf1 x) b s1u<s1x)  record { fcy<sup = zc13
+... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ?  record { fcy<sup = zc13
 ; order = zc17 ; supu=u = zc18   } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b)))  ) ⟫ where
 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px )
 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc )
 zc18 : supf1 px ≡ px
 zc18 = begin
 zc12 {z} sfpx=px sfpx<sp (case2 fc) = zc21 fc where
 --- supf0 px o< sp1
 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
 zc21 {z1} (fsuc z2 fc ) with zc21 fc
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫
-zc21 (init asp refl ) =  ⟪ asp , ch-is-sup px zc18
+zc21 (init asp refl ) =  ⟪ asp , ch-is-sup px ?
 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
 zc15 : supf1 px ≡ px
 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
 zc18 : supf1 px o< supf1 x
 zc18 = subst₂ ( λ j k → j o< k ) (sym (sf1=sf0 o≤-refl)) (sym (sf1=sp1 px<x)) sfpx<sp
 csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) (
 UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤
 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x)
 (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
 -- px o< z1 , px o≤ supf1 z1  -->   px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1
+--      supf1 px ≡ sp1 o< supf1 x
 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
 csupf1 {z1} sz1<x = csupf2 where
 --  z1 o< px → supf1 z1 ≡ supf0 z1
 --  z1 ≡ px , supf0 px o< px   .. px o< z1, x o≤ z1 ...  supf1 z1 ≡ sp1
 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} ⟪ 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
 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩
 supf0 u ≡⟨ ? ⟩
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay supf x) f b  →
 * a < * b → odef (UnionCF A f mf ay supf x) b
 is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
-... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab ,
+... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ? -- ⟪ ab ,
 -- subst (λ k → UChain A f mf ay supf x k )
---     (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
+--     (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫
 zc70 : HasPrev A pchain f x  → ¬ xSUP pchain f x
 zc70 pr xsup = ?
 no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) supf0 x ) → ZChain A f mf ay x
 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
 pchain0=1 : pchain ≡ pchain1
 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where
+zc10 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc12 fc where
 zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
 zc12 (fsuc x fc) with zc12 fc
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
 zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫
 zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where
+zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where
 zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
 zc13 (fsuc x fc) with zc13 fc
 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
+... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
 zc13 (init asu su=z ) with trio< u x
 ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫
 ... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c )
+... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u≤x c )
 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
 sup {z} z≤x with trio< z x
 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
 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
+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))
 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 )))
+z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A ? (fsuc _ ( fsuc  _ fc )))
 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 supf 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
+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
 z48 : supf mc << d
 z48 = sc<<d {mc} asc spd
 z53 : supf u o< supf (& A)
-z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) )
+z53 = ordtrans<-≤ u≤x ?
 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)) ⟫
+, ch-is-sup u ? is-sup1 (init (ZChain.asupf zc)  (ChainP.supu=u is-sup1)) ⟫
 z51 : supf u o≤ supf mc
 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
 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 ))
+z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A ? (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 (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
 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 ⟫ = 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)
+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) )
+z53 = ordtrans<-≤ u≤x ?
 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)) ⟫
+, ch-is-sup u ? 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
 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
+-- u≤x    : ZChain.supf zc u o< ZChain.supf zc d
 --     supf u o< supf c → order
 sd=d : supf d ≡ d
 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫

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

comparison src/zorn.agda @ 979:6229017a6176