Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1068:f24f4de4d459
add 0<supfz
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 13 Dec 2022 02:59:01 +0900 |
parents | 074b6a506b1b |
children | 99df080f4fdb |
comparison
equal
deleted
inserted
replaced
1067:074b6a506b1b | 1068:f24f4de4d459 |
---|---|
348 | 348 |
349 asupf : {x : Ordinal } → odef A (supf x) | 349 asupf : {x : Ordinal } → odef A (supf x) |
350 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y | 350 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y |
351 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z | 351 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z |
352 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x | 352 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x |
353 0<supfz : {x : Ordinal } → o∅ o< supf x | |
353 | 354 |
354 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) | 355 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) |
355 | 356 |
356 chain : HOD | 357 chain : HOD |
357 chain = UnionCF A f ay supf z | 358 chain = UnionCF A f ay supf z |
883 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where | 884 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where |
884 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) | 885 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) |
885 m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz) | 886 m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz) |
886 | 887 |
887 zc41 : ZChain A f mf< ay x | 888 zc41 : ZChain A f mf< ay x |
888 zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order | 889 zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order ; 0<supfz = ? |
889 ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ; cfcs = cfcs } where | 890 ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ; cfcs = cfcs } where |
890 | 891 |
891 supf1 : Ordinal → Ordinal | 892 supf1 : Ordinal → Ordinal |
892 supf1 z with trio< z px | 893 supf1 z with trio< z px |
893 ... | tri< a ¬b ¬c = supf0 z | 894 ... | tri< a ¬b ¬c = supf0 z |
1236 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) | 1237 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) |
1237 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1 | 1238 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1 |
1238 | 1239 |
1239 ... | no lim with trio< x o∅ | 1240 ... | no lim with trio< x o∅ |
1240 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 1241 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1241 ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) | 1242 ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? |
1242 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) | 1243 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) |
1243 ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where | 1244 ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where |
1244 mf : ≤-monotonic-f A f | 1245 mf : ≤-monotonic-f A f |
1245 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where | 1246 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where |
1246 mf00 : * x < * (f x) | 1247 mf00 : * x < * (f x) |
1247 mf00 = proj1 ( mf< x ax ) | 1248 mf00 = proj1 ( mf< x ax ) |
1248 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? | 1249 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ? |
1249 ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where | 1250 ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where |
1250 | 1251 |
1251 -- mf : ≤-monotonic-f A f | 1252 -- mf : ≤-monotonic-f A f |
1252 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust | 1253 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust |
1253 | 1254 |
1318 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin | 1319 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin |
1319 ZChain.supf (pzc (pic<x ib)) (IChain-i ib) ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc) ⟩ | 1320 ZChain.supf (pzc (pic<x ib)) (IChain-i ib) ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc) ⟩ |
1320 ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ | 1321 ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ |
1321 ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O | 1322 ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O |
1322 | 1323 |
1324 IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b ) | |
1325 → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a | |
1326 IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫ | |
1327 IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where | |
1328 ic02 : o∅ o< supfz i<x | |
1329 ic02 = ZChain.0<supfz (pzc (ob<x lim i<x)) | |
1330 ic01 : o∅ o< i | |
1331 ic01 = ordtrans<-≤ ic02 sa<x | |
1332 IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib | |
1333 = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x) | |
1334 (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc ) | |
1335 | |
1323 ptotalx : IsTotalOrderSet pchainx | 1336 ptotalx : IsTotalOrderSet pchainx |
1324 ptotalx {a} {b} ia ib with trio< (ZChain.supf (pzc (pic<x (proj2 ia))) (IChain-i (proj2 ia))) | 1337 ptotalx {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib)) |
1325 (ZChain.supf (pzc (pic<x (proj2 ib))) (IChain-i (proj2 ib))) | 1338 ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainx⊆chain ib) |
1326 ... | tri< ia<ib ¬b ¬c = uz01 where | 1339 ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainx⊆chain ib) |
1327 uz01 : Tri (a < b) (a ≡ b) (b < a ) | 1340 ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia)) |
1328 uz01 with pchainx⊆chain ia | |
1329 ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib) | |
1330 ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u uz02 uz03 uz04 ⟫ (pchainx⊆chain ib) where | |
1331 a<b : IChain-i (proj2 ia) o< IChain-i (proj2 ib) | |
1332 a<b = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib | |
1333 uz02 : u o< osuc (IChain-i (proj2 ib)) | |
1334 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b)) | |
1335 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u | |
1336 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u | |
1337 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a) | |
1338 uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc | |
1339 ... | tri≈ ¬a ia=ib ¬c = ? where | |
1340 uz01 : Tri (* (& a ) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a )) | |
1341 uz01 with proj2 ia | proj2 ib | |
1342 ... | ic-init fca | ic-init fcb = fcn-cmp y f mf fca fcb | |
1343 ... | ic-isup ia ia<x sa<x fca | ic-init fcb = ? | |
1344 ... | ic-init fca | ic-isup ib ib<x sb<x fcb = ? | |
1345 ... | ic-isup ia ia<x sa<x fca | ic-isup ib ib<x sb<x fcb = fcn-cmp ? f mf ? ? | |
1346 ... | tri> ¬a ¬b ib<ia = uz01 where | |
1347 uz01 : Tri (a < b) (a ≡ b) (b < a ) | |
1348 uz01 with pchainx⊆chain ib | |
1349 ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-init fc ⟫ | |
1350 ... | ⟪ bi , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-is-sup u uz02 uz03 uz04 ⟫ where | |
1351 b<a : IChain-i (proj2 ib) o< IChain-i (proj2 ia) | |
1352 b<a = ichain-inject {_} {_} {proj2 ib} {proj2 ia} ib<ia | |
1353 uz02 : u o< osuc (IChain-i (proj2 ia)) | |
1354 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc b<a)) | |
1355 uz03 : ZChain.supf (pzc (pic<x (proj2 ia))) u ≡ u | |
1356 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) )) su=u | |
1357 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ia))) u) (& b) | |
1358 uz04 = subst (λ k → FClosure A f k (& b)) ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) ) fc | |
1359 | 1341 |
1360 usup : MinSUP A pchainx | 1342 usup : MinSUP A pchainx |
1361 usup = minsupP pchainx (λ ic → ? ) ptotalx | 1343 usup = minsupP pchainx (λ ic → ? ) ptotalx |
1362 spu = MinSUP.sup usup | 1344 spu = MinSUP.sup usup |
1363 | 1345 |