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

comparison OD.agda @ 408:3ac3704b4cb1

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 Tue, 28 Jul 2020 22:34:42 +0900
parents 349d4e734403
children 3fba5f805e50
comparison
equal deleted inserted replaced
407:349d4e734403 408:3ac3704b4cb1
516 ω-prev-eq : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y 516 ω-prev-eq : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
517 ω-prev-eq {x} {y} eq with trio< x y 517 ω-prev-eq {x} {y} eq with trio< x y
518 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a) 518 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
519 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b 519 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
520 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) 520 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
521
522 ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x
523 ω-∈s x not = not (od→ord (x , x)) record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord x) ) (sym oiso) (case1 refl) }
521 524
522 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 525 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
523 nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where 526 nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where
524 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) → 527 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
525 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x 528 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
541 (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } ) 544 (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
542 lemma1 : infinite ∋ ord→od x₁ 545 lemma1 : infinite ∋ ord→od x₁
543 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd 546 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
544 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1 547 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
545 lemma3 iφ iφ refl = HE.refl 548 lemma3 iφ iφ refl = HE.refl
546 lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ? ) 549 lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso eq (c<→o< (ω-∈s (ord→od y)) )))
547 lemma3 (isuc ltd) iφ eq = {!!} 550 lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso (sym eq) (c<→o< (ω-∈s (ord→od y)) )))
548 lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq)) 551 lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
549 ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t 552 ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t
550 lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1 553 lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
551 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where 554 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where
552 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 555 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1