Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 950:6e126013f056
...
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