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

comparison HOD.agda @ 169:acbcbd98d588

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
trans finite on ε-induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Jul 2019 05:12:08 +0900
parents b25a4eca06a6
children c96f28c3c387
comparison
equal deleted inserted replaced
168:b25a4eca06a6 169:acbcbd98d588
472 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} 472 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}
473 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) 473 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x )
474 → (x : OD {suc n} ) → ψ x 474 → (x : OD {suc n} ) → ψ x
475 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where 475 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where
476 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) 476 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy)
477 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case1 ()) 477 ε-induction-ord ox = TransFinite {suc n} {suc n ⊔ m} {λ z → {oy : Ordinal {suc n} } → oy o< z → ψ (ord→od oy) } lemma1 lemma2 ox where
478 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case2 ()) 478 lemma1 : (lx : Nat) {oy : Ordinal} → oy o< record { lv = lx ; ord = Φ lx } → ψ (ord→od oy)
479 ε-induction-ord record { lv = lx ; ord = (OSuc lx ox) } {oy} y<x = 479 lemma1 Zero {oy} (case1 ())
480 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where 480 lemma1 Zero {oy} (case2 ())
481 lemma : (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox } 481 lemma1 (Suc lx) {record { lv = Zero ; ord = Φ 0 }} (case1 (s≤s z≤n)) = {!!}
482 lemma y lt with osuc-≡< y<x 482 lemma1 (Suc lx) {record { lv = Zero ; ord = OSuc 0 oy }} (case1 (s≤s z≤n)) = {!!}
483 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso 483 lemma1 (Suc (Suc lx)) {record { lv = Suc ly ; ord = Φ (Suc ly) }} (case1 (s≤s (s≤s x))) = {!!}
484 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 484 lemma1 (Suc (Suc lx)) {record { lv = Suc ly ; ord = OSuc (Suc ly) oy }} (case1 (s≤s (s≤s x))) = {!!}
485 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = OSuc ly oy }} (case1 (s≤s x)) = 485 lemma2 : (lx : Nat) (x₁ : OrdinalD lx) →
486 ind {ord→od record { lv = ly ; ord = OSuc ly oy }} ( 486 ({oy : Ordinal} → oy o< record { lv = lx ; ord = x₁ } → ψ (ord→od oy)) →
487 λ {y} lt → subst ( λ k → ψ k ) oiso ( ε-induction-ord record { lv = lx ; ord = (Φ lx) } {od→ord y} {!!})) where 487 {oy : Ordinal} → oy o< record { lv = lx ; ord = OSuc lx x₁ } → ψ (ord→od oy)
488 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = Φ ly }} (case1 (s≤s x)) = {!!} 488 lemma2 lx x1 p lt = ind ( λ {y} lty → subst (λ k → ψ k) oiso (p {!!} ))
489 489