Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1073:b3d695340773
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 14 Dec 2022 11:21:16 +0900 |
| parents | 4ce084a0dce2 |
| children | 1e7d20b15341 |
comparison
equal
deleted
inserted
replaced
| 1072:4ce084a0dce2 | 1073:b3d695340773 |
|---|---|
| 1465 | 1465 |
| 1466 0<sufz : {x : Ordinal } → o∅ o< supf1 x | 1466 0<sufz : {x : Ordinal } → o∅ o< supf1 x |
| 1467 0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z)) | 1467 0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z)) |
| 1468 | 1468 |
| 1469 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) | 1469 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) |
| 1470 is-minsup = ? | 1470 is-minsup {z} z≤x with osuc-≡< z≤x |
| 1471 ... | case1 z=x = ? | |
| 1472 ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where | |
| 1473 supf0 = ZChain.supf (pzc (ob<x lim z<x)) | |
| 1474 msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z) | |
| 1475 msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) | |
| 1476 zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z | |
| 1477 zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup ⟪ az , ch-init fc ⟫ ) -- U supf0 | |
| 1478 zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) | |
| 1479 ( IsMinSUP.x≤sup msup ⟪ az , ch-is-sup u u<b ? ? ⟫ ) -- U supf0 | |
| 1480 zm01 : { s : Ordinal } → odef A s → ( {x : Ordinal } → odef (UnionCF A f ay supf1 z) x → x ≤ s ) → supf1 z o≤ s | |
| 1481 zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where -- U supf1 | |
| 1482 zm02 : {w : Ordinal } → odef (UnionCF A f ay supf0 z) w → w ≤ s | |
| 1483 zm02 {w} ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ | |
| 1484 zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup ⟪ az , ch-is-sup u u<b ? ? ⟫ | |
| 1485 | |
| 1486 | |
| 1471 | 1487 |
| 1472 cfcs : {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w | 1488 cfcs : {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w |
| 1473 cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x | 1489 cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x |
| 1474 ... | case1 b=x with trio< a x | 1490 ... | case1 b=x with trio< a x |
| 1475 ... | tri< a<x ¬b ¬c = zc40 where | 1491 ... | tri< a<x ¬b ¬c = zc40 where |