Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 768:67c7d4b43844
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 25 Jul 2022 22:53:11 +0900 |
parents | 6c87cb98abf2 |
children | 34678c0ad278 |
files | src/zorn.agda |
diffstat | 1 files changed, 6 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jul 25 22:27:15 2022 +0900 +++ b/src/zorn.agda Mon Jul 25 22:53:11 2022 +0900 @@ -645,10 +645,7 @@ ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where spi = & (SUP.sup (ysup f mf ay)) isupf : Ordinal → Ordinal - isupf z with trio< z spi - ... | tri< a ¬b ¬c = y - ... | tri≈ ¬a b ¬c = spi - ... | tri> ¬a ¬b c = spi + isupf z = spi sp = ysup f mf ay asi = SUP.A∋maximal sp cy : odef (UnionCF A f mf ay isupf o∅) y @@ -658,7 +655,7 @@ isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z isy {z} ⟪ az , uz ⟫ with uz ... | ch-init fc = s≤fc y f mf fc - ... | ch-is-sup u is-sup fc = ? + ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc ) inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a) inext {a} ua with (proj2 ua) ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫ @@ -669,9 +666,8 @@ uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb) csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z) - csupf {z} = uz00 where - -- = ? where -- ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where - uz03 : {z : Ordinal } → FClosure A f y z → (z ≡ spi) ∨ (z << spi) + csupf {z} = ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where + uz03 : {z : Ordinal } → FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi) uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc ) ... | case1 eq = case1 ( begin z ≡⟨ sym &iso ⟩ @@ -680,13 +676,8 @@ ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt ) uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi) uz04 {s} {z} s<spi fcz = ? - -- uz02 : ChainP A f mf ay isupf spi spi - -- uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? } - uz00 : odef (UnionCF A f mf ay isupf o∅) (isupf z) - uz00 with trio< z spi - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + uz02 : ChainP A f mf ay isupf spi (isupf z) + uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? } --