Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 984:9fe534223348
order s o< t is bad
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 11 Nov 2022 23:57:58 +0900 |
| parents | 6101b9bfbe57 |
| children | |
| files | src/zorn.agda |
| diffstat | 1 files changed, 14 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Nov 11 21:48:38 2022 +0900 +++ b/src/zorn.agda Fri Nov 11 23:57:58 2022 +0900 @@ -647,9 +647,12 @@ ... | ⟪ 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 → s o< 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 ? fc )) - -- supf (supf b) ≡ supf b + sp = MinSUP.sup (ZChain.minsup zc (o<→≤ b<z)) + zc00 : ( z1 ≡ sp ) ∨ ( z1 << sp ) + zc00 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ss<sb)) + ... | case2 lt = 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 lt fc )) + ... | case1 eq = ? -- subst (λ k → ( z1 ≡ k ) ∨ ( z1 << k ) ) ? ( ≤to<= ( s≤fc {A} _ f mf fc ) ) zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) zc04 with zc00 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq ) @@ -682,9 +685,9 @@ m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b - m09 {s} {z} s<b fcz = order b<A ? fcz + m09 {s} {z} s<b fcz = order b<A (ZChain.supf-inject zc s<b) fcz m06 : ChainP A f mf ay supf b - m06 = record { fcy<sup = m08 ; order = ? ; supu=u = m05 } + m06 = record { fcy<sup = m08 ; order = order b<A ; supu=u = m05 } ... | no lim = record { is-max = is-max ; order = order } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → @@ -703,7 +706,7 @@ m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b - m08 {s} {z1} s<b fc = order m09 ? fc + m08 {s} {z1} s<b fc = order m09 (ZChain.supf-inject zc s<b) fc m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) @@ -711,7 +714,7 @@ m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b - m06 = record { fcy<sup = m07 ; order = ? ; supu=u = m05 } + m06 = record { fcy<sup = m07 ; order = order m09 ; supu=u = m05 } uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = @@ -1413,7 +1416,7 @@ 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 ? (fsuc _ ( fsuc _ fc ))) + z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (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 ) } @@ -1446,9 +1449,9 @@ 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 ? (fsuc _ ( fsuc _ fc )) + z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A (ZChain.supf-inject zc 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 ? (fsuc _ ( fsuc _ fc )) + 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 @@ -1491,8 +1494,7 @@ 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 - ? fc ) smc<<d ) - -- (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1)) u<smc) fc ) smc<<d ) + (ZChain.supf-inject zc (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