Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 330:0faa7120e4b5
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 15:49:00 +0900 |
parents | 5544f4921a44 |
children | feb0fcc430a9 |
line wrap: on
line diff
--- a/ordinal.agda Sun Jul 05 12:32:09 2020 +0900 +++ b/ordinal.agda Sun Jul 05 15:49:00 2020 +0900 @@ -219,6 +219,7 @@ ; <-osuc = <-osuc ; osuc-≡< = osuc-≡< ; TransFinite = TransFinite1 + ; TransFinite1 = TransFinite2 ; not-limit = not-limit ; next-limit = next-limit } @@ -244,4 +245,15 @@ caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → ψ (record { lv = lx ; ord = OSuc lx x₁ }) caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev + TransFinite2 : { ψ : ord1 → Set (suc (suc n)) } + → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord1) → ψ x + TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where + caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → + ψ (record { lv = lx ; ord = Φ lx }) + caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev + caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → + ψ (record { lv = lx ; ord = OSuc lx x₁ }) + caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev +