Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 847:bf1b6c4768d2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 03 Sep 2022 13:28:10 +0900 |
| parents | 95bbeb622f6e |
| children | 56a150965988 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 13 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Sep 03 09:43:19 2022 +0900 +++ b/src/zorn.agda Sat Sep 03 13:28:10 2022 +0900 @@ -973,11 +973,22 @@ csupf1 with csupf0 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ - = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = ? } ? ⟫ where + = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = supu=u1 } ? ⟫ where + zc13 : supf0 u o< supf0 b + zc13 = ? + zc12 : odef (UnionCF A f mf ay supf0 b) (supf1 b) + zc12 = subst (λ k → odef (UnionCF A f mf ay supf0 b) k) &iso ( ZChain.csupf-fc zc b≤px zc13 fc ) u≤x1 : u o≤ supf1 b u≤x1 = u≤x + supu=u0 : supf0 u ≡ u + supu=u0 = supu=u supu=u1 : supf1 u ≡ u - supu=u1 = ? + supu=u1 with trio< u px + ... | tri< a ¬b ¬c = supu=u + ... | tri≈ ¬a b ¬c = supu=u + ... | tri> ¬a ¬b c = ? -- supf1 b ≡ sp1 , u o≤ sp1, x o≤ u o≤ supf1 b -- u ≡ x → xsup x → ⊥ + -- u > x → supf1 u ≡ sp1 → supf1 b o≤ supf1 u + -- px o< u o≤ sp1 , spuf1 u o≤ spuf1 sp1 fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) fcy<sup1 = ? order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1