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

comparison ordinal.agda @ 329:5544f4921a44

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 12:32:09 +0900
parents 1a54dbe1ea4c
children 0faa7120e4b5
comparison
equal deleted inserted replaced
328:72f3e3b44c27 329:5544f4921a44
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 ; next = next
215 ; isOrdinal = record { 215 ; isOrdinal = record {
216 Otrans = ordtrans 216 Otrans = ordtrans
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 ; is-limit = {!!} 222 ; not-limit = not-limit
223 ; next-limit = {!!} 223 ; next-limit = next-limit
224 } 224 }
225 } where 225 } where
226 next : Ordinal {suc n} → Ordinal {suc n}
227 next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
228 next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
229 next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
230 lemma : (x : Ordinal) → x o< next y → osuc x o< next y
231 lemma x (case1 lt) = case1 lt
232 not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
233 not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
234 not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
226 ord1 : Set (suc n) 235 ord1 : Set (suc n)
227 ord1 = Ordinal {suc n} 236 ord1 = Ordinal {suc n}
228 TransFinite1 : { ψ : ord1 → Set (suc n) } 237 TransFinite1 : { ψ : ord1 → Set (suc n) }
229 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) 238 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x )
230 → ∀ (x : ord1) → ψ x 239 → ∀ (x : ord1) → ψ x