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

comparison ordinal.agda @ 330:0faa7120e4b5

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, 05 Jul 2020 15:49:00 +0900
parents 5544f4921a44
children feb0fcc430a9
comparison
equal deleted inserted replaced
329:5544f4921a44 330:0faa7120e4b5
217 ; OTri = trio< 217 ; OTri = trio<
218 ; ¬x<0 = ¬x<0 218 ; ¬x<0 = ¬x<0
219 ; <-osuc = <-osuc 219 ; <-osuc = <-osuc
220 ; osuc-≡< = osuc-≡< 220 ; osuc-≡< = osuc-≡<
221 ; TransFinite = TransFinite1 221 ; TransFinite = TransFinite1
222 ; TransFinite1 = TransFinite2
222 ; not-limit = not-limit 223 ; not-limit = not-limit
223 ; next-limit = next-limit 224 ; next-limit = next-limit
224 } 225 }
225 } where 226 } where
226 next : Ordinal {suc n} → Ordinal {suc n} 227 next : Ordinal {suc n} → Ordinal {suc n}
242 ψ (record { lv = lx ; ord = Φ lx }) 243 ψ (record { lv = lx ; ord = Φ lx })
243 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev 244 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
244 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → 245 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
245 ψ (record { lv = lx ; ord = OSuc lx x₁ }) 246 ψ (record { lv = lx ; ord = OSuc lx x₁ })
246 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 247 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev
247 248 TransFinite2 : { ψ : ord1 → Set (suc (suc n)) }
249 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x )
250 → ∀ (x : ord1) → ψ x
251 TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
252 caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
253 ψ (record { lv = lx ; ord = Φ lx })
254 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
255 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
256 ψ (record { lv = lx ; ord = OSuc lx x₁ })
257 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev
258
259