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

comparison OD.agda @ 393:43b0a6ca7602

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 Sun, 26 Jul 2020 21:10:37 +0900
parents 19687f3304c9
children 77c6123f49ee
comparison
equal deleted inserted replaced
392:55f44ec2a0c6 393:43b0a6ca7602
235 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) ) 235 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
236 pair-xx<xy {x} {y} = ⊆→o≤ lemma where 236 pair-xx<xy {x} {y} = ⊆→o≤ lemma where
237 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z 237 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
238 lemma {z} (case1 refl) = case1 refl 238 lemma {z} (case1 refl) = case1 refl
239 lemma {z} (case2 refl) = case1 refl 239 lemma {z} (case2 refl) = case1 refl
240
241 pair-<xy : {x y : HOD} → {n : Ordinal} → od→ord x o< next n → od→ord y o< next n → od→ord (x , y) o< next n
242 pair-<xy {x} {y} {o} x<nn y<nn with trio< (od→ord x) (od→ord y) | inspect (omax (od→ord x)) (od→ord y)
243 ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
244 ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
245 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
240 246
241 -- another form of infinite 247 -- another form of infinite
242 -- pair-ord< : {x : Ordinal } → Set n 248 -- pair-ord< : {x : Ordinal } → Set n
243 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x) 249 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
244 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where 250 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where
425 --- main recursion 431 --- main recursion
426 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 432 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
427 lemma {o∅} iφ = x<nx 433 lemma {o∅} iφ = x<nx
428 lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) 434 lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
429 435
430 ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ 436 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
431 ω<next-o∅ ho< {y} lt = <odmax infinite lt 437 ω<next-o∅ {y} lt = <odmax infinite lt
432 438
433 nat→ω : Nat → HOD 439 nat→ω : Nat → HOD
434 nat→ω Zero = od∅ 440 nat→ω Zero = od∅
435 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 441 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
436 442