Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 329:5544f4921a44
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 12:32:09 +0900 |
parents | 1a54dbe1ea4c |
children | 0faa7120e4b5 |
line wrap: on
line diff
--- a/ordinal.agda Sun Jul 05 11:40:55 2020 +0900 +++ b/ordinal.agda Sun Jul 05 12:32:09 2020 +0900 @@ -211,7 +211,7 @@ ; o∅ = o∅ ; osuc = osuc ; _o<_ = _o<_ - ; next = {!!} + ; next = next ; isOrdinal = record { Otrans = ordtrans ; OTri = trio< @@ -219,10 +219,19 @@ ; <-osuc = <-osuc ; osuc-≡< = osuc-≡< ; TransFinite = TransFinite1 - ; is-limit = {!!} - ; next-limit = {!!} + ; not-limit = not-limit + ; next-limit = next-limit } } where + next : Ordinal {suc n} → Ordinal {suc n} + next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv)) + next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) + next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where + lemma : (x : Ordinal) → x o< next y → osuc x o< next y + lemma x (case1 lt) = case1 lt + not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y))) + not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () )) + not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl ) ord1 : Set (suc n) ord1 = Ordinal {suc n} TransFinite1 : { ψ : ord1 → Set (suc n) }