Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 325:1a54dbe1ea4c
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 04 Jul 2020 22:48:49 +0900 |
parents | fbabb20f222e |
children | feeba7fd499a |
files | OD.agda ordinal.agda |
diffstat | 2 files changed, 9 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Sat Jul 04 18:18:17 2020 +0900 +++ b/OD.agda Sat Jul 04 22:48:49 2020 +0900 @@ -329,14 +329,17 @@ lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt } lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x)) )) lemma3 {x} = od⊆→o≤ lemma1 + lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x)) + lemma4 {x} = ordtrans (<odmax (x , x) {!!}) {!!} lemma : {y : Ordinal} → infinite-d y → y o< next o∅ lemma {y} = TransFinite {λ x → infinite-d x → x o< next o∅ } ind y where ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅)) → infinite-d x → x o< (next o∅) ind o∅ prev iφ = proj1 next-limit - ind x prev (isuc lt) = lemma0 where - lemma0 : {x : Ordinal} → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ - lemma0 {x} = {!!} + ind x prev (isuc lt) = lemma0 {_} {x} {!!} where + lemma0 : {x z : Ordinal} → x o< od→ord (Union (ord→od z , (ord→od z , ord→od z))) → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ + lemma0 {x} with prev x {!!} + ... | t = {!!} _=h=_ : (x y : HOD) → Set n x =h= y = od x == od y
--- a/ordinal.agda Sat Jul 04 18:18:17 2020 +0900 +++ b/ordinal.agda Sat Jul 04 22:48:49 2020 +0900 @@ -211,7 +211,7 @@ ; o∅ = o∅ ; osuc = osuc ; _o<_ = _o<_ - ; next = ? + ; next = {!!} ; isOrdinal = record { Otrans = ordtrans ; OTri = trio< @@ -219,8 +219,8 @@ ; <-osuc = <-osuc ; osuc-≡< = osuc-≡< ; TransFinite = TransFinite1 - ; is-limit = ? - ; next-limit = ? + ; is-limit = {!!} + ; next-limit = {!!} } } where ord1 : Set (suc n)