Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 323:e228e96965f0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Jul 2020 12:53:40 +0900
parents a9d380378efd
children fbabb20f222e
comparison
equal deleted inserted replaced
322:a9d380378efd 323:e228e96965f0
313 data infinite-d : ( x : Ordinal ) → Set n where 313 data infinite-d : ( x : Ordinal ) → Set n where
314 iφ : infinite-d o∅ 314 iφ : infinite-d o∅
315 isuc : {x : Ordinal } → infinite-d x → 315 isuc : {x : Ordinal } → infinite-d x →
316 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 316 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
317 317
318 is-ω : (x : Ordinal) → Dec (infinite-d x )
319 is-ω x = {!!}
320
318 infinite : HOD 321 infinite : HOD
319 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 322 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma1 } where
320 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 323 lemma : {y : Ordinal} → Lift (suc n) (infinite-d y → y o< next o∅ )
321 lemma {o∅} iφ = proj1 next-limit 324 lemma {y} = TransFinite {λ x → Lift (suc n) (infinite-d x → x o< next o∅) } ind y where
322 lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i ) 325 ind : (x : Ordinal) → ((z : Ordinal) → z o< x → Lift (suc n) (infinite-d z → z o< (next o∅))) →
323 lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ 326 Lift (suc n) (infinite-d x → x o< (next o∅))
324 lemma1 = {!!} 327 ind x prev with {!!}
325 328 ... | ttt = {!!}
326 329 lemma1 : {y : Ordinal} → infinite-d y → y o< next o∅
330 lemma1 {y} with lemma {y}
331 lemma1 {y} | lift p = p
327 332
328 _=h=_ : (x y : HOD) → Set n 333 _=h=_ : (x y : HOD) → Set n
329 x =h= y = od x == od y 334 x =h= y = od x == od y
330 335
331 infixr 200 _∈_ 336 infixr 200 _∈_