Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1053:a281ad683577
order connected
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 09 Dec 2022 20:53:59 +0900 |
parents | 0b6cee971cba |
children | 38148b08d85c |
comparison
equal
deleted
inserted
replaced
1052:0b6cee971cba | 1053:a281ad683577 |
---|---|
473 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b | 473 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b |
474 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) | 474 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) |
475 ... | case2 lt = lt | 475 ... | case2 lt = lt |
476 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) | 476 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) |
477 | 477 |
478 supfeq : {a b : Ordinal } → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b | 478 supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b |
479 supfeq = ? | 479 supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b) |
480 | 480 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( |
481 unioneq : {a b : Ordinal } → z o≤ supf a → supf a o≤ supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b | 481 IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) |
482 unioneq = ? | 482 ... | tri≈ ¬a b ¬c = b |
483 | 483 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( |
484 -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b) | 484 IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) |
485 -- the condition of cfcs is satisfied, this is obvious | 485 |
486 union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b | |
487 union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where | |
488 z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w | |
489 z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
490 z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where | |
491 u<b : u o< b | |
492 u<b = ordtrans u<a (supf-inject sa<sb ) | |
493 z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w | |
494 z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
495 z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where | |
496 u<a : u o< a | |
497 u<a = supf-inject ( osucprev (begin | |
498 osuc (supf u) ≡⟨ cong osuc su=u ⟩ | |
499 osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ | |
500 z ≤⟨ z≤sa ⟩ | |
501 supf a ∎ )) where open o≤-Reasoning O | |
486 | 502 |
487 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) | 503 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) |
488 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where | 504 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where |
489 supf = ZChain.supf zc | 505 supf = ZChain.supf zc |
490 field | 506 field |
1182 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc45 c ) --- supf0 px o≤ supf1 x ≡ sp1 | 1198 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc45 c ) --- supf0 px o≤ supf1 x ≡ sp1 |
1183 zc40 : f (supf0 px) ≤ supf0 px | 1199 zc40 : f (supf0 px) ≤ supf0 px |
1184 zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) | 1200 zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) |
1185 ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫ )) | 1201 ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫ )) |
1186 | 1202 |
1203 supfeq1 : {a b : Ordinal } → a o≤ x → b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b | |
1204 supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b) | |
1205 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( | |
1206 IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) | |
1207 ... | tri≈ ¬a b ¬c = b | |
1208 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( | |
1209 IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) | |
1210 | |
1211 union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b | |
1212 union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where | |
1213 z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w | |
1214 z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
1215 z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where | |
1216 u<b : u o< b | |
1217 u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb ) | |
1218 z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w | |
1219 z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ | |
1220 z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where | |
1221 u<a : u o< a | |
1222 u<a = supf-inject0 supf1-mono ( osucprev (begin | |
1223 osuc (supf1 u) ≡⟨ cong osuc su=u ⟩ | |
1224 osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ | |
1225 x ≤⟨ z≤sa ⟩ | |
1226 supf1 a ∎ )) where open o≤-Reasoning O | |
1227 | |
1187 order : {a b : Ordinal} {w : Ordinal} → | 1228 order : {a b : Ordinal} {w : Ordinal} → |
1188 b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b | 1229 b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b |
1189 order {a} {b} {w} b≤x sa<sb fc = z20 where | 1230 order {a} {b} {w} b≤x sa<sb fc = z20 where |
1190 a<b : a o< b | 1231 a<b : a o< b |
1191 a<b = supf-inject0 supf1-mono sa<sb | 1232 a<b = supf-inject0 supf1-mono sa<sb |
1200 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) | 1241 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) |
1201 (fcup fc (o<→≤ (ordtrans a<b b<px))) | 1242 (fcup fc (o<→≤ (ordtrans a<b b<px))) |
1202 ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where | 1243 ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where |
1203 z26 : odef ( UnionCF A f ay supf0 b ) w | 1244 z26 : odef ( UnionCF A f ay supf0 b ) w |
1204 z26 with x<y∨y≤x (supf1 a) b | 1245 z26 with x<y∨y≤x (supf1 a) b |
1205 ... | case2 b≤sa = ? | 1246 ... | case2 b≤sa = ⊥-elim ( o<¬≡ ( supfeq1 ? ? ( union-max1 ? ? (subst (λ k → supf1 a o< k) ? sa<sb) )) |
1247 (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 ?)) ))) | |
1206 ... | case1 sa<b with cfcs a<b b≤x sa<b fc | 1248 ... | case1 sa<b with cfcs a<b b≤x sa<b fc |
1207 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ | 1249 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ |
1208 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫ | 1250 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫ |
1209 ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b | 1251 ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b |
1210 ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) | 1252 ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) |
1211 ... | case2 b≤sa = ? -- x=b x o≤ sa UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥ | 1253 ... | case2 b≤sa = ⊥-elim ( o<¬≡ ? sa<sb ) where -- x=b x o≤ sa UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥ |
1254 b=x : b ≡ x | |
1255 b=x with trio< b x | |
1256 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ a ⟫ ) -- px o< b o< x | |
1257 ... | tri≈ ¬a b ¬c = b | |
1258 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b ≤ x | |
1259 z27 : supf1 a ≡ supf1 b | |
1260 z27 = supfeq1 ? ? ( union-max1 ? ? sa<sb ) | |
1212 | 1261 |
1213 ... | no lim with trio< x o∅ | 1262 ... | no lim with trio< x o∅ |
1214 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 1263 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1215 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ? | 1264 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ? |
1216 ; supfmax = ? ; is-minsup = ? ; cfcs = ? } | 1265 ; supfmax = ? ; is-minsup = ? ; cfcs = ? } |