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

comparison ordinal.agda @ 324:fbabb20f222e

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 Sat, 04 Jul 2020 18:18:17 +0900
parents 6f10c47e4e7a
children 1a54dbe1ea4c
comparison
equal deleted inserted replaced
323:e228e96965f0 324:fbabb20f222e
209 C-Ordinal {n} = record { 209 C-Ordinal {n} = record {
210 ord = Ordinal {suc n} 210 ord = Ordinal {suc n}
211 ; o∅ = o∅ 211 ; o∅ = o∅
212 ; osuc = osuc 212 ; osuc = osuc
213 ; _o<_ = _o<_ 213 ; _o<_ = _o<_
214 ; next = ?
214 ; isOrdinal = record { 215 ; isOrdinal = record {
215 Otrans = ordtrans 216 Otrans = ordtrans
216 ; OTri = trio< 217 ; OTri = trio<
217 ; ¬x<0 = ¬x<0 218 ; ¬x<0 = ¬x<0
218 ; <-osuc = <-osuc 219 ; <-osuc = <-osuc
219 ; osuc-≡< = osuc-≡< 220 ; osuc-≡< = osuc-≡<
220 ; TransFinite = TransFinite1 221 ; TransFinite = TransFinite1
222 ; is-limit = ?
223 ; next-limit = ?
221 } 224 }
222 } where 225 } where
223 ord1 : Set (suc n) 226 ord1 : Set (suc n)
224 ord1 = Ordinal {suc n} 227 ord1 = Ordinal {suc n}
225 TransFinite1 : { ψ : ord1 → Set (suc (suc n)) } 228 TransFinite1 : { ψ : ord1 → Set (suc n) }
226 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) 229 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x )
227 → ∀ (x : ord1) → ψ x 230 → ∀ (x : ord1) → ψ x
228 TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where 231 TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
229 caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → 232 caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
230 ψ (record { lv = lx ; ord = Φ lx }) 233 ψ (record { lv = lx ; ord = Φ lx })
231 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev 234 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
232 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → 235 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
233 ψ (record { lv = lx ; ord = OSuc lx x₁ }) 236 ψ (record { lv = lx ; ord = OSuc lx x₁ })